Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadadd2lem2 Structured version   Visualization version   GIF version

 Description: The core of the proof of sadadd2 15020. The intuitive justification for this is that cadd is true if at least two arguments are true, and hadd is true if an odd number of arguments are true, so altogether the result is 𝑛 · 𝐴 where 𝑛 is the number of true arguments, which is equivalently obtained by adding together one 𝐴 for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016.)
Assertion
Ref Expression
sadadd2lem2 (𝐴 ∈ ℂ → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))

StepHypRef Expression
1 0cn 9911 . . . . . . . . 9 0 ∈ ℂ
2 ifcl 4080 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜓, 𝐴, 0) ∈ ℂ)
31, 2mpan2 703 . . . . . . . 8 (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ)
43ad2antrr 758 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
5 simpll 786 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ)
64, 5, 5add12d 10141 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
75, 4, 5addassd 9941 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
86, 7eqtr4d 2647 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
9 pm5.501 355 . . . . . . . . 9 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
109adantl 481 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
1110bicomd 212 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑𝜓) ↔ 𝜓))
1211ifbid 4058 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
13 simpr 476 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝜑)
1413orcd 406 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑𝜓))
15 iftrue 4042 . . . . . . . 8 ((𝜑𝜓) → if((𝜑𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
1614, 15syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
1752timesd 11152 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴))
1816, 17eqtrd 2644 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴))
1912, 18oveq12d 6567 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)))
20 iftrue 4042 . . . . . . . 8 (𝜑 → if(𝜑, 𝐴, 0) = 𝐴)
2120adantl 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
2221oveq1d 6564 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
2322oveq1d 6564 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
248, 19, 233eqtr4d 2654 . . . 4 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
25 iffalse 4045 . . . . . . . . 9 𝜑 → if(𝜑, 𝐴, 0) = 0)
2625adantl 481 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
2726oveq1d 6564 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
283ad2antrr 758 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
2928addid2d 10116 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
3027, 29eqtrd 2644 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
3130oveq1d 6564 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴))
32 2cnd 10970 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → 2 ∈ ℂ)
33 id 22 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
3432, 33mulcld 9939 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
3534addid2d 10116 . . . . . . . . . 10 (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (2 · 𝐴))
36 2times 11022 . . . . . . . . . 10 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3735, 36eqtrd 2644 . . . . . . . . 9 (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
3837adantr 480 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
39 iftrue 4042 . . . . . . . . . 10 (𝜓 → if(𝜓, 0, 𝐴) = 0)
4039adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0)
41 iftrue 4042 . . . . . . . . . 10 (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
4241adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
4340, 42oveq12d 6567 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴)))
44 iftrue 4042 . . . . . . . . . 10 (𝜓 → if(𝜓, 𝐴, 0) = 𝐴)
4544adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴)
4645oveq1d 6564 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴))
4738, 43, 463eqtr4d 2654 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
48 simpl 472 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 𝐴 ∈ ℂ)
49 0cnd 9912 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 0 ∈ ℂ)
5048, 49addcomd 10117 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (𝐴 + 0) = (0 + 𝐴))
51 iffalse 4045 . . . . . . . . . 10 𝜓 → if(𝜓, 0, 𝐴) = 𝐴)
5251adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 0, 𝐴) = 𝐴)
53 iffalse 4045 . . . . . . . . . 10 𝜓 → if(𝜓, (2 · 𝐴), 0) = 0)
5453adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = 0)
5552, 54oveq12d 6567 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0))
56 iffalse 4045 . . . . . . . . . 10 𝜓 → if(𝜓, 𝐴, 0) = 0)
5756adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 𝐴, 0) = 0)
5857oveq1d 6564 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴))
5950, 55, 583eqtr4d 2654 . . . . . . 7 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
6047, 59pm2.61dan 828 . . . . . 6 (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
6160ad2antrr 758 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
62 ifnot 4083 . . . . . . 7 if(¬ 𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴)
63 nbn2 359 . . . . . . . . 9 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
6463adantl 481 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
6564ifbid 4058 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
6662, 65syl5eqr 2658 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑𝜓), 𝐴, 0))
67 biorf 419 . . . . . . . 8 𝜑 → (𝜓 ↔ (𝜑𝜓)))
6867adantl 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
6968ifbid 4058 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
7066, 69oveq12d 6567 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
7131, 61, 703eqtr2rd 2651 . . . 4 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
7224, 71pm2.61dan 828 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
73 hadrot 1531 . . . . . . 7 (hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒))
74 had1 1533 . . . . . . 7 (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑𝜓)))
7573, 74syl5bbr 273 . . . . . 6 (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7675adantl 481 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7776ifbid 4058 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
78 cad1 1546 . . . . . 6 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7978adantl 481 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
8079ifbid 4058 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
8177, 80oveq12d 6567 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
82 iftrue 4042 . . . . 5 (𝜒 → if(𝜒, 𝐴, 0) = 𝐴)
8382adantl 481 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴)
8483oveq2d 6565 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
8572, 81, 843eqtr4d 2654 . 2 ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
8620adantl 481 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
8786oveq1d 6564 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
8845oveq2d 6565 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴))
8938, 43, 883eqtr4d 2654 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9054, 57eqtr4d 2647 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0))
9152, 90oveq12d 6567 . . . . . . 7 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9289, 91pm2.61dan 828 . . . . . 6 (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9392ad2antrr 758 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
949adantl 481 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
9594notbid 307 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑𝜓)))
96 df-xor 1457 . . . . . . . . 9 ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
9795, 96syl6bbr 277 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
9897ifbid 4058 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
9962, 98syl5eqr 2658 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑𝜓), 𝐴, 0))
100 ibar 524 . . . . . . . 8 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
101100adantl 481 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
102101ifbid 4058 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
10399, 102oveq12d 6567 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
10487, 93, 1033eqtr2rd 2651 . . . 4 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
105 simplll 794 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ)
106 0cnd 9912 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ)
107105, 106ifclda 4070 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
108 0cnd 9912 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → 0 ∈ ℂ)
109107, 108addcomd 10117 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 𝐴, 0) + 0) = (0 + if(𝜓, 𝐴, 0)))
11063adantl 481 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
111110con1bid 344 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ (𝜑𝜓) ↔ 𝜓))
11296, 111syl5bb 271 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ((𝜑𝜓) ↔ 𝜓))
113112ifbid 4058 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
114 simpr 476 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ 𝜑)
115114intnanrd 954 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ (𝜑𝜓))
116 iffalse 4045 . . . . . . 7 (¬ (𝜑𝜓) → if((𝜑𝜓), (2 · 𝐴), 0) = 0)
117115, 116syl 17 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = 0)
118113, 117oveq12d 6567 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0))
11925adantl 481 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
120119oveq1d 6564 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
121109, 118, 1203eqtr4d 2654 . . . 4 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
122104, 121pm2.61dan 828 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
123 had0 1534 . . . . . . 7 𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑𝜓)))
12473, 123syl5bbr 273 . . . . . 6 𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
125124adantl 481 . . . . 5 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
126125ifbid 4058 . . . 4 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
127 cad0 1547 . . . . . 6 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
128127adantl 481 . . . . 5 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
129128ifbid 4058 . . . 4 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
130126, 129oveq12d 6567 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
131 iffalse 4045 . . . . 5 𝜒 → if(𝜒, 𝐴, 0) = 0)
132131oveq2d 6565 . . . 4 𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0))
133 ifcl 4080 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜑, 𝐴, 0) ∈ ℂ)
1341, 133mpan2 703 . . . . . 6 (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ)
135134, 3addcld 9938 . . . . 5 (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ)
136135addid1d 10115 . . . 4 (𝐴 ∈ ℂ → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
137132, 136sylan9eqr 2666 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
138122, 130, 1373eqtr4d 2654 . 2 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
13985, 138pm2.61dan 828 1 (𝐴 ∈ ℂ → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))