Proof of Theorem sadadd2lem2
Step | Hyp | Ref
| Expression |
1 | | 0cn 10967 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
2 | | ifcl 4504 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝜓, 𝐴, 0) ∈
ℂ) |
3 | 1, 2 | mpan2 688 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → if(𝜓, 𝐴, 0) ∈ ℂ) |
4 | 3 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ) |
5 | | simpll 764 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → 𝐴 ∈ ℂ) |
6 | 4, 5, 5 | add12d 11201 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴))) |
7 | 5, 4, 5 | addassd 10997 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴) = (𝐴 + (if(𝜓, 𝐴, 0) + 𝐴))) |
8 | 6, 7 | eqtr4d 2781 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴)) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴)) |
9 | | pm5.501 367 |
. . . . . . . . 9
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
10 | 9 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
11 | 10 | bicomd 222 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((𝜑 ↔ 𝜓) ↔ 𝜓)) |
12 | 11 | ifbid 4482 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ↔ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0)) |
13 | | animorrl 978 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (𝜑 ∨ 𝜓)) |
14 | | iftrue 4465 |
. . . . . . . 8
⊢ ((𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴)) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (2 · 𝐴)) |
16 | 5 | 2timesd 12216 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (2 · 𝐴) = (𝐴 + 𝐴)) |
17 | 15, 16 | eqtrd 2778 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if((𝜑 ∨ 𝜓), (2 · 𝐴), 0) = (𝐴 + 𝐴)) |
18 | 12, 17 | oveq12d 7293 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + (𝐴 + 𝐴))) |
19 | | iftrue 4465 |
. . . . . . . 8
⊢ (𝜑 → if(𝜑, 𝐴, 0) = 𝐴) |
20 | 19 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴) |
21 | 20 | oveq1d 7290 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
22 | 21 | oveq1d 7290 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = ((𝐴 + if(𝜓, 𝐴, 0)) + 𝐴)) |
23 | 8, 18, 22 | 3eqtr4d 2788 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
24 | | iffalse 4468 |
. . . . . . . . 9
⊢ (¬
𝜑 → if(𝜑, 𝐴, 0) = 0) |
25 | 24 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0) |
26 | 25 | oveq1d 7290 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0))) |
27 | 3 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ) |
28 | 27 | addid2d 11176 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (0 + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0)) |
29 | 26, 28 | eqtrd 2778 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = if(𝜓, 𝐴, 0)) |
30 | 29 | oveq1d 7290 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴) = (if(𝜓, 𝐴, 0) + 𝐴)) |
31 | | 2cnd 12051 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 2 ∈
ℂ) |
32 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
33 | 31, 32 | mulcld 10995 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → (2
· 𝐴) ∈
ℂ) |
34 | 33 | addid2d 11176 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (0 + (2
· 𝐴)) = (2 ·
𝐴)) |
35 | | 2times 12109 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ → (2
· 𝐴) = (𝐴 + 𝐴)) |
36 | 34, 35 | eqtrd 2778 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (0 + (2
· 𝐴)) = (𝐴 + 𝐴)) |
37 | 36 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (0 + (2 · 𝐴)) = (𝐴 + 𝐴)) |
38 | | iftrue 4465 |
. . . . . . . . . 10
⊢ (𝜓 → if(𝜓, 0, 𝐴) = 0) |
39 | 38 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 0, 𝐴) = 0) |
40 | | iftrue 4465 |
. . . . . . . . . 10
⊢ (𝜓 → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴)) |
41 | 40 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, (2 · 𝐴), 0) = (2 · 𝐴)) |
42 | 39, 41 | oveq12d 7293 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (0 + (2 · 𝐴))) |
43 | | iftrue 4465 |
. . . . . . . . . 10
⊢ (𝜓 → if(𝜓, 𝐴, 0) = 𝐴) |
44 | 43 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → if(𝜓, 𝐴, 0) = 𝐴) |
45 | 44 | oveq1d 7290 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (𝐴 + 𝐴)) |
46 | 37, 42, 45 | 3eqtr4d 2788 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
47 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → 𝐴 ∈ ℂ) |
48 | | 0cnd 10968 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → 0 ∈
ℂ) |
49 | 47, 48 | addcomd 11177 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (𝐴 + 0) = (0 + 𝐴)) |
50 | | iffalse 4468 |
. . . . . . . . . 10
⊢ (¬
𝜓 → if(𝜓, 0, 𝐴) = 𝐴) |
51 | 50 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, 0, 𝐴) = 𝐴) |
52 | | iffalse 4468 |
. . . . . . . . . 10
⊢ (¬
𝜓 → if(𝜓, (2 · 𝐴), 0) = 0) |
53 | 52 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, (2 · 𝐴), 0) = 0) |
54 | 51, 53 | oveq12d 7293 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + 0)) |
55 | | iffalse 4468 |
. . . . . . . . . 10
⊢ (¬
𝜓 → if(𝜓, 𝐴, 0) = 0) |
56 | 55 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, 𝐴, 0) = 0) |
57 | 56 | oveq1d 7290 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 𝐴, 0) + 𝐴) = (0 + 𝐴)) |
58 | 49, 54, 57 | 3eqtr4d 2788 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
59 | 46, 58 | pm2.61dan 810 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
60 | 59 | ad2antrr 723 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 𝐴)) |
61 | | ifnot 4511 |
. . . . . . 7
⊢ if(¬
𝜓, 𝐴, 0) = if(𝜓, 0, 𝐴) |
62 | | nbn2 371 |
. . . . . . . . 9
⊢ (¬
𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
63 | 62 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
64 | 63 | ifbid 4482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0)) |
65 | 61, 64 | eqtr3id 2792 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ↔ 𝜓), 𝐴, 0)) |
66 | | biorf 934 |
. . . . . . . 8
⊢ (¬
𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
67 | 66 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
68 | 67 | ifbid 4482 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) |
69 | 65, 68 | oveq12d 7293 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))) |
70 | 30, 60, 69 | 3eqtr2rd 2785 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝜒) ∧ ¬ 𝜑) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
71 | 23, 70 | pm2.61dan 810 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
72 | | hadrot 1603 |
. . . . . . 7
⊢
(hadd(𝜒, 𝜑, 𝜓) ↔ hadd(𝜑, 𝜓, 𝜒)) |
73 | | had1 1605 |
. . . . . . 7
⊢ (𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ↔ 𝜓))) |
74 | 72, 73 | bitr3id 285 |
. . . . . 6
⊢ (𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓))) |
75 | 74 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ 𝜓))) |
76 | 75 | ifbid 4482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ↔ 𝜓), 𝐴, 0)) |
77 | | cad1 1619 |
. . . . . 6
⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) |
78 | 77 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) |
79 | 78 | ifbid 4482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∨ 𝜓), (2 · 𝐴), 0)) |
80 | 76, 79 | oveq12d 7293 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ↔ 𝜓), 𝐴, 0) + if((𝜑 ∨ 𝜓), (2 · 𝐴), 0))) |
81 | | iftrue 4465 |
. . . . 5
⊢ (𝜒 → if(𝜒, 𝐴, 0) = 𝐴) |
82 | 81 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → if(𝜒, 𝐴, 0) = 𝐴) |
83 | 82 | oveq2d 7291 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 𝐴)) |
84 | 71, 80, 83 | 3eqtr4d 2788 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0))) |
85 | 19 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(𝜑, 𝐴, 0) = 𝐴) |
86 | 85 | oveq1d 7290 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
87 | 44 | oveq2d 7291 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (𝐴 + if(𝜓, 𝐴, 0)) = (𝐴 + 𝐴)) |
88 | 37, 42, 87 | 3eqtr4d 2788 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
89 | 53, 56 | eqtr4d 2781 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → if(𝜓, (2 · 𝐴), 0) = if(𝜓, 𝐴, 0)) |
90 | 51, 89 | oveq12d 7293 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜓) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
91 | 88, 90 | pm2.61dan 810 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
92 | 91 | ad2antrr 723 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (𝐴 + if(𝜓, 𝐴, 0))) |
93 | 9 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
94 | 93 | notbid 318 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ ¬ (𝜑 ↔ 𝜓))) |
95 | | df-xor 1507 |
. . . . . . . . 9
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) |
96 | 94, 95 | bitr4di 289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (¬ 𝜓 ↔ (𝜑 ⊻ 𝜓))) |
97 | 96 | ifbid 4482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(¬ 𝜓, 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0)) |
98 | 61, 97 | eqtr3id 2792 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(𝜓, 0, 𝐴) = if((𝜑 ⊻ 𝜓), 𝐴, 0)) |
99 | | ibar 529 |
. . . . . . . 8
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
100 | 99 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
101 | 100 | ifbid 4482 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → if(𝜓, (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) |
102 | 98, 101 | oveq12d 7293 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if(𝜓, 0, 𝐴) + if(𝜓, (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))) |
103 | 86, 92, 102 | 3eqtr2rd 2785 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
104 | | simplll 772 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) ∧ 𝜓) → 𝐴 ∈ ℂ) |
105 | | 0cnd 10968 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) ∧ ¬ 𝜓) → 0 ∈ ℂ) |
106 | 104, 105 | ifclda 4494 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if(𝜓, 𝐴, 0) ∈ ℂ) |
107 | | 0cnd 10968 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → 0 ∈
ℂ) |
108 | 106, 107 | addcomd 11177 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if(𝜓, 𝐴, 0) + 0) = (0 + if(𝜓, 𝐴, 0))) |
109 | 62 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
110 | 109 | con1bid 356 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (¬ (𝜑 ↔ 𝜓) ↔ 𝜓)) |
111 | 95, 110 | bitrid 282 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → ((𝜑 ⊻ 𝜓) ↔ 𝜓)) |
112 | 111 | ifbid 4482 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if((𝜑 ⊻ 𝜓), 𝐴, 0) = if(𝜓, 𝐴, 0)) |
113 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → ¬ 𝜑) |
114 | 113 | intnanrd 490 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → ¬ (𝜑 ∧ 𝜓)) |
115 | | iffalse 4468 |
. . . . . . 7
⊢ (¬
(𝜑 ∧ 𝜓) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0) |
116 | 114, 115 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if((𝜑 ∧ 𝜓), (2 · 𝐴), 0) = 0) |
117 | 112, 116 | oveq12d 7293 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜓, 𝐴, 0) + 0)) |
118 | 24 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → if(𝜑, 𝐴, 0) = 0) |
119 | 118 | oveq1d 7290 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) = (0 + if(𝜓, 𝐴, 0))) |
120 | 108, 117,
119 | 3eqtr4d 2788 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ ¬
𝜒) ∧ ¬ 𝜑) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
121 | 103, 120 | pm2.61dan 810 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
122 | | had0 1606 |
. . . . . . 7
⊢ (¬
𝜒 → (hadd(𝜒, 𝜑, 𝜓) ↔ (𝜑 ⊻ 𝜓))) |
123 | 72, 122 | bitr3id 285 |
. . . . . 6
⊢ (¬
𝜒 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓))) |
124 | 123 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ 𝜓))) |
125 | 124 | ifbid 4482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) = if((𝜑 ⊻ 𝜓), 𝐴, 0)) |
126 | | cad0 1620 |
. . . . . 6
⊢ (¬
𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) |
127 | 126 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) |
128 | 127 | ifbid 4482 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0) = if((𝜑 ∧ 𝜓), (2 · 𝐴), 0)) |
129 | 125, 128 | oveq12d 7293 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = (if((𝜑 ⊻ 𝜓), 𝐴, 0) + if((𝜑 ∧ 𝜓), (2 · 𝐴), 0))) |
130 | | iffalse 4468 |
. . . . 5
⊢ (¬
𝜒 → if(𝜒, 𝐴, 0) = 0) |
131 | 130 | oveq2d 7291 |
. . . 4
⊢ (¬
𝜒 → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0)) |
132 | | ifcl 4504 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → if(𝜑, 𝐴, 0) ∈
ℂ) |
133 | 1, 132 | mpan2 688 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → if(𝜑, 𝐴, 0) ∈ ℂ) |
134 | 133, 3 | addcld 10994 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) ∈ ℂ) |
135 | 134 | addid1d 11175 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + 0) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
136 | 131, 135 | sylan9eqr 2800 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0)) = (if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0))) |
137 | 121, 129,
136 | 3eqtr4d 2788 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝜒) → (if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0))) |
138 | 84, 137 | pm2.61dan 810 |
1
⊢ (𝐴 ∈ ℂ →
(if(hadd(𝜑, 𝜓, 𝜒), 𝐴, 0) + if(cadd(𝜑, 𝜓, 𝜒), (2 · 𝐴), 0)) = ((if(𝜑, 𝐴, 0) + if(𝜓, 𝐴, 0)) + if(𝜒, 𝐴, 0))) |