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

Theorem sadadd2lem2 16330
Description: The core of the proof of sadadd2 16340. 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 11147 . . . . . . . . 9 0 ∈ ℂ
2 ifcl 4531 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜓, 𝐴, 0) ∈ ℂ)
31, 2mpan2 689 . . . . . . . 8 (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ)
43ad2antrr 724 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
5 simpll 765 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ)
64, 5, 5add12d 11381 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
75, 4, 5addassd 11177 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴)))
86, 7eqtr4d 2779 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
9 pm5.501 366 . . . . . . . . 9 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
109adantl 482 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
1110bicomd 222 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑𝜓) ↔ 𝜓))
1211ifbid 4509 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
13 animorrl 979 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑𝜓))
14 iftrue 4492 . . . . . . . 8 ((𝜑𝜓) → if((𝜑𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
1513, 14syl 17 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = (2 · 𝐴))
1652timesd 12396 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴))
1715, 16eqtrd 2776 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴))
1812, 17oveq12d 7375 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)))
19 iftrue 4492 . . . . . . . 8 (𝜑 → if(𝜑, 𝐴, 0) = 𝐴)
2019adantl 482 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
2120oveq1d 7372 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
2221oveq1d 7372 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴))
238, 18, 223eqtr4d 2786 . . . 4 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
24 iffalse 4495 . . . . . . . . 9 𝜑 → if(𝜑, 𝐴, 0) = 0)
2524adantl 482 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
2625oveq1d 7372 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
273ad2antrr 724 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
2827addid2d 11356 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
2926, 28eqtrd 2776 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0))
3029oveq1d 7372 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴))
31 2cnd 12231 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → 2 ∈ ℂ)
32 id 22 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
3331, 32mulcld 11175 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
3433addid2d 11356 . . . . . . . . . 10 (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (2 · 𝐴))
35 2times 12289 . . . . . . . . . 10 (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
3634, 35eqtrd 2776 . . . . . . . . 9 (𝐴 ∈ ℂ → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
3736adantr 481 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴))
38 iftrue 4492 . . . . . . . . . 10 (𝜓 → if(𝜓, 0, 𝐴) = 0)
3938adantl 482 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0)
40 iftrue 4492 . . . . . . . . . 10 (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
4140adantl 482 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴))
4239, 41oveq12d 7375 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴)))
43 iftrue 4492 . . . . . . . . . 10 (𝜓 → if(𝜓, 𝐴, 0) = 𝐴)
4443adantl 482 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴)
4544oveq1d 7372 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴))
4637, 42, 453eqtr4d 2786 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
47 simpl 483 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 𝐴 ∈ ℂ)
48 0cnd 11148 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → 0 ∈ ℂ)
4947, 48addcomd 11357 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (𝐴 + 0) = (0 + 𝐴))
50 iffalse 4495 . . . . . . . . . 10 𝜓 → if(𝜓, 0, 𝐴) = 𝐴)
5150adantl 482 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 0, 𝐴) = 𝐴)
52 iffalse 4495 . . . . . . . . . 10 𝜓 → if(𝜓, (2 · 𝐴), 0) = 0)
5352adantl 482 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = 0)
5451, 53oveq12d 7375 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0))
55 iffalse 4495 . . . . . . . . . 10 𝜓 → if(𝜓, 𝐴, 0) = 0)
5655adantl 482 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, 𝐴, 0) = 0)
5756oveq1d 7372 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴))
5849, 54, 573eqtr4d 2786 . . . . . . 7 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
5946, 58pm2.61dan 811 . . . . . 6 (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
6059ad2antrr 724 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴))
61 ifnot 4538 . . . . . . 7 if(¬ 𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴)
62 nbn2 370 . . . . . . . . 9 𝜑 → (¬ 𝜓 ↔ (𝜑𝜓)))
6362adantl 482 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
6463ifbid 4509 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
6561, 64eqtr3id 2790 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑𝜓), 𝐴, 0))
66 biorf 935 . . . . . . . 8 𝜑 → (𝜓 ↔ (𝜑𝜓)))
6766adantl 482 . . . . . . 7 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
6867ifbid 4509 . . . . . 6 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
6965, 68oveq12d 7375 . . . . 5 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
7030, 60, 693eqtr2rd 2783 . . . 4 (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
7123, 70pm2.61dan 811 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
72 hadrot 1602 . . . . . . 7 (hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒))
73 had1 1604 . . . . . . 7 (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑𝜓)))
7472, 73bitr3id 284 . . . . . 6 (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7574adantl 482 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7675ifbid 4509 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
77 cad1 1618 . . . . . 6 (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7877adantl 482 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
7978ifbid 4509 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
8076, 79oveq12d 7375 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
81 iftrue 4492 . . . . 5 (𝜒 → if(𝜒, 𝐴, 0) = 𝐴)
8281adantl 482 . . . 4 ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴)
8382oveq2d 7373 . . 3 ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴))
8471, 80, 833eqtr4d 2786 . 2 ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
8519adantl 482 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴)
8685oveq1d 7372 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
8744oveq2d 7373 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴))
8837, 42, 873eqtr4d 2786 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
8953, 56eqtr4d 2779 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0))
9051, 89oveq12d 7375 . . . . . . 7 ((𝐴 ∈ ℂ ∧ ¬ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9188, 90pm2.61dan 811 . . . . . 6 (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
9291ad2antrr 724 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0)))
939adantl 482 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
9493notbid 317 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑𝜓)))
95 df-xor 1510 . . . . . . . . 9 ((𝜑𝜓) ↔ ¬ (𝜑𝜓))
9694, 95bitr4di 288 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
9796ifbid 4509 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
9861, 97eqtr3id 2790 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑𝜓), 𝐴, 0))
99 ibar 529 . . . . . . . 8 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
10099adantl 482 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑𝜓)))
101100ifbid 4509 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
10298, 101oveq12d 7375 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
10386, 92, 1023eqtr2rd 2783 . . . 4 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
104 simplll 773 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ)
105 0cnd 11148 . . . . . . 7 ((((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ)
106104, 105ifclda 4521 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ)
107 0cnd 11148 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → 0 ∈ ℂ)
108106, 107addcomd 11357 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 𝐴, 0) + 0) = (0 + if(𝜓, 𝐴, 0)))
10962adantl 482 . . . . . . . . 9 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑𝜓)))
110109con1bid 355 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (¬ (𝜑𝜓) ↔ 𝜓))
11195, 110bitrid 282 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ((𝜑𝜓) ↔ 𝜓))
112111ifbid 4509 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0))
113 simpr 485 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ 𝜑)
114113intnanrd 490 . . . . . . 7 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → ¬ (𝜑𝜓))
115 iffalse 4495 . . . . . . 7 (¬ (𝜑𝜓) → if((𝜑𝜓), (2 · 𝐴), 0) = 0)
116114, 115syl 17 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if((𝜑𝜓), (2 · 𝐴), 0) = 0)
117112, 116oveq12d 7375 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0))
11824adantl 482 . . . . . 6 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0)
119118oveq1d 7372 . . . . 5 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0)))
120108, 117, 1193eqtr4d 2786 . . . 4 (((𝐴 ∈ ℂ ∧ ¬ 𝜒) ∧ ¬ 𝜑) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
121103, 120pm2.61dan 811 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
122 had0 1605 . . . . . . 7 𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑𝜓)))
12372, 122bitr3id 284 . . . . . 6 𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
124123adantl 482 . . . . 5 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
125124ifbid 4509 . . . 4 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑𝜓), 𝐴, 0))
126 cad0 1619 . . . . . 6 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
127126adantl 482 . . . . 5 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
128127ifbid 4509 . . . 4 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑𝜓), (2 · 𝐴), 0))
129125, 128oveq12d 7375 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑𝜓), 𝐴, 0) + if((𝜑𝜓), (2 · 𝐴), 0)))
130 iffalse 4495 . . . . 5 𝜒 → if(𝜒, 𝐴, 0) = 0)
131130oveq2d 7373 . . . 4 𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0))
132 ifcl 4531 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → if(𝜑, 𝐴, 0) ∈ ℂ)
1331, 132mpan2 689 . . . . . 6 (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ)
134133, 3addcld 11174 . . . . 5 (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ)
135134addid1d 11355 . . . 4 (𝐴 ∈ ℂ → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
136131, 135sylan9eqr 2798 . . 3 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)))
137121, 129, 1363eqtr4d 2786 . 2 ((𝐴 ∈ ℂ ∧ ¬ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)))
13884, 137pm2.61dan 811 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 205  wa 396  wo 845  wxo 1509   = wceq 1541  haddwhad 1594  caddwcad 1607  wcel 2106  ifcif 4486  (class class class)co 7357  cc 11049  0cc0 11051   + caddc 11054   · cmul 11056  2c2 12208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-xor 1510  df-tru 1544  df-fal 1554  df-had 1595  df-cad 1608  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-ltxr 11194  df-2 12216
This theorem is referenced by:  sadadd2lem  16339
  Copyright terms: Public domain W3C validator