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

Theorem sadadd2lem2 15380
Description: The core of the proof of sadadd2 15390. 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)))

Proof of Theorem sadadd2lem2
StepHypRef Expression
1 0cn 10234 . . . . . . . . 9 0 ∈ ℂ
2 ifcl 4269 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜓, 𝐴, 0) ∈ ℂ)
31, 2mpan2 671 . . . . . . . 8 (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ)
43ad2antrr 705 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
5 simpll 750 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ)
64, 5, 5add12d 10464 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
75, 4, 5addassd 10264 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
86, 7eqtr4d 2808 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
9 pm5.501 355 . . . . . . . . 9 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
109adantl 467 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
1110bicomd 213 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑𝜓) ↔ 𝜓))
1211ifbid 4247 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
13 simpr 471 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝜑)
1413orcd 860 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑𝜓))
15 iftrue 4231 . . . . . . . 8 ((𝜑𝜓) → if((𝜑𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
1614, 15syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
1752timesd 11477 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴))
1816, 17eqtrd 2805 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴))
1912, 18oveq12d 6811 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)))
20 iftrue 4231 . . . . . . . 8 (𝜑 → if(𝜑, 𝐴, 0) = 𝐴)
2120adantl 467 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
2221oveq1d 6808 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
2322oveq1d 6808 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
248, 19, 233eqtr4d 2815 . . . 4 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
25 iffalse 4234 . . . . . . . . 9 𝜑 → if(𝜑, 𝐴, 0) = 0)
2625adantl 467 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
2726oveq1d 6808 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
283ad2antrr 705 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
2928addid2d 10439 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
3027, 29eqtrd 2805 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
3130oveq1d 6808 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴))
32 2cnd 11295 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → 2 ∈ ℂ)
33 id 22 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
3432, 33mulcld 10262 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
3534addid2d 10439 . . . . . . . . . 10 (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (2 · 𝐴))
36 2times 11347 . . . . . . . . . 10 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3735, 36eqtrd 2805 . . . . . . . . 9 (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
3837adantr 466 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
39 iftrue 4231 . . . . . . . . . 10 (𝜓 → if(𝜓, 0, 𝐴) = 0)
4039adantl 467 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0)
41 iftrue 4231 . . . . . . . . . 10 (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
4241adantl 467 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
4340, 42oveq12d 6811 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴)))
44 iftrue 4231 . . . . . . . . . 10 (𝜓 → if(𝜓, 𝐴, 0) = 𝐴)
4544adantl 467 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴)
4645oveq1d 6808 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴))
4738, 43, 463eqtr4d 2815 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
48 simpl 468 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 𝐴 ∈ ℂ)
49 0cnd 10235 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 0 ∈ ℂ)
5048, 49addcomd 10440 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (𝐴 + 0) = (0 + 𝐴))
51 iffalse 4234 . . . . . . . . . 10 𝜓 → if(𝜓, 0, 𝐴) = 𝐴)
5251adantl 467 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 0, 𝐴) = 𝐴)
53 iffalse 4234 . . . . . . . . . 10 𝜓 → if(𝜓, (2 · 𝐴), 0) = 0)
5453adantl 467 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = 0)
5552, 54oveq12d 6811 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0))
56 iffalse 4234 . . . . . . . . . 10 𝜓 → if(𝜓, 𝐴, 0) = 0)
5756adantl 467 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 𝐴, 0) = 0)
5857oveq1d 6808 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴))
5950, 55, 583eqtr4d 2815 . . . . . . 7 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
6047, 59pm2.61dan 813 . . . . . 6 (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
6160ad2antrr 705 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
62 ifnot 4272 . . . . . . 7 if(¬ 𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴)
63 nbn2 359 . . . . . . . . 9 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
6463adantl 467 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
6564ifbid 4247 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
6662, 65syl5eqr 2819 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑𝜓), 𝐴, 0))
67 biorf 920 . . . . . . . 8 𝜑 → (𝜓 ↔ (𝜑𝜓)))
6867adantl 467 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
6968ifbid 4247 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
7066, 69oveq12d 6811 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
7131, 61, 703eqtr2rd 2812 . . . 4 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
7224, 71pm2.61dan 813 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
73 hadrot 1688 . . . . . . 7 (hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒))
74 had1 1690 . . . . . . 7 (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑𝜓)))
7573, 74syl5bbr 274 . . . . . 6 (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7675adantl 467 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7776ifbid 4247 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
78 cad1 1703 . . . . . 6 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7978adantl 467 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
8079ifbid 4247 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
8177, 80oveq12d 6811 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
82 iftrue 4231 . . . . 5 (𝜒 → if(𝜒, 𝐴, 0) = 𝐴)
8382adantl 467 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴)
8483oveq2d 6809 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
8572, 81, 843eqtr4d 2815 . 2 ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
8620adantl 467 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
8786oveq1d 6808 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
8845oveq2d 6809 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴))
8938, 43, 883eqtr4d 2815 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9054, 57eqtr4d 2808 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0))
9152, 90oveq12d 6811 . . . . . . 7 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9289, 91pm2.61dan 813 . . . . . 6 (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9392ad2antrr 705 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
949adantl 467 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
9594notbid 307 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑𝜓)))
96 df-xor 1613 . . . . . . . . 9 ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
9795, 96syl6bbr 278 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
9897ifbid 4247 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
9962, 98syl5eqr 2819 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑𝜓), 𝐴, 0))
100 ibar 518 . . . . . . . 8 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
101100adantl 467 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
102101ifbid 4247 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
10399, 102oveq12d 6811 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
10487, 93, 1033eqtr2rd 2812 . . . 4 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
105 simplll 758 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ)
106 0cnd 10235 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ)
107105, 106ifclda 4259 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
108 0cnd 10235 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → 0 ∈ ℂ)
109107, 108addcomd 10440 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 𝐴, 0) + 0) = (0 + if(𝜓, 𝐴, 0)))
11063adantl 467 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
111110con1bid 344 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ (𝜑𝜓) ↔ 𝜓))
11296, 111syl5bb 272 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ((𝜑𝜓) ↔ 𝜓))
113112ifbid 4247 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
114 simpr 471 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ 𝜑)
115114intnanrd 477 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ (𝜑𝜓))
116 iffalse 4234 . . . . . . 7 (¬ (𝜑𝜓) → if((𝜑𝜓), (2 · 𝐴), 0) = 0)
117115, 116syl 17 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = 0)
118113, 117oveq12d 6811 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0))
11925adantl 467 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
120119oveq1d 6808 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
121109, 118, 1203eqtr4d 2815 . . . 4 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
122104, 121pm2.61dan 813 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
123 had0 1691 . . . . . . 7 𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑𝜓)))
12473, 123syl5bbr 274 . . . . . 6 𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
125124adantl 467 . . . . 5 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
126125ifbid 4247 . . . 4 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
127 cad0 1704 . . . . . 6 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
128127adantl 467 . . . . 5 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
129128ifbid 4247 . . . 4 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
130126, 129oveq12d 6811 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
131 iffalse 4234 . . . . 5 𝜒 → if(𝜒, 𝐴, 0) = 0)
132131oveq2d 6809 . . . 4 𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0))
133 ifcl 4269 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜑, 𝐴, 0) ∈ ℂ)
1341, 133mpan2 671 . . . . . 6 (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ)
135134, 3addcld 10261 . . . . 5 (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ)
136135addid1d 10438 . . . 4 (𝐴 ∈ ℂ → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
137132, 136sylan9eqr 2827 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
138122, 130, 1373eqtr4d 2815 . 2 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
13985, 138pm2.61dan 813 1 (𝐴 ∈ ℂ → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 834  wxo 1612   = wceq 1631  haddwhad 1680  caddwcad 1693  wcel 2145  ifcif 4225  (class class class)co 6793  cc 10136  0cc0 10138   + caddc 10141   · cmul 10143  2c2 11272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-xor 1613  df-tru 1634  df-had 1681  df-cad 1694  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-ov 6796  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-ltxr 10281  df-2 11281
This theorem is referenced by:  sadadd2lem  15389
  Copyright terms: Public domain W3C validator