Metamath Proof Explorer


Theorem sadadd2lem2

Description: The core of the proof of sadadd2 . 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 n x. A where n is the number of true arguments, which is equivalently obtained by adding together one A for each true argument, on the right side. (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Assertion sadadd2lem2 ( 𝐴 ∈ ℂ → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 0cn 0 ∈ ℂ
2 ifcl ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
3 1 2 mpan2 ( 𝐴 ∈ ℂ → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
4 3 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
5 simpll ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → 𝐴 ∈ ℂ )
6 4 5 5 add12d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) = ( 𝐴 + ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) ) )
7 5 4 5 addassd ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( 𝐴 + ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) ) )
8 6 7 eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) = ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
9 pm5.501 ( 𝜑 → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
10 9 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
11 10 bicomd ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( 𝜑𝜓 ) ↔ 𝜓 ) )
12 11 ifbid ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
13 animorrl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 𝜑𝜓 ) )
14 iftrue ( ( 𝜑𝜓 ) → if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
15 13 14 syl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
16 5 2timesd ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
17 15 16 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) = ( 𝐴 + 𝐴 ) )
18 12 17 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + ( 𝐴 + 𝐴 ) ) )
19 iftrue ( 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
20 19 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
21 20 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
22 21 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
23 8 18 22 3eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
24 iffalse ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 0 ) = 0 )
25 24 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 0 )
26 25 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
27 3 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
28 27 addid2d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) = if ( 𝜓 , 𝐴 , 0 ) )
29 26 28 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = if ( 𝜓 , 𝐴 , 0 ) )
30 29 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
31 2cnd ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
32 id ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
33 31 32 mulcld ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
34 33 addid2d ( 𝐴 ∈ ℂ → ( 0 + ( 2 · 𝐴 ) ) = ( 2 · 𝐴 ) )
35 2times ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
36 34 35 eqtrd ( 𝐴 ∈ ℂ → ( 0 + ( 2 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
37 36 adantr ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( 0 + ( 2 · 𝐴 ) ) = ( 𝐴 + 𝐴 ) )
38 iftrue ( 𝜓 → if ( 𝜓 , 0 , 𝐴 ) = 0 )
39 38 adantl ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , 0 , 𝐴 ) = 0 )
40 iftrue ( 𝜓 → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
41 40 adantl ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = ( 2 · 𝐴 ) )
42 39 41 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 0 + ( 2 · 𝐴 ) ) )
43 iftrue ( 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
44 43 adantl ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → if ( 𝜓 , 𝐴 , 0 ) = 𝐴 )
45 44 oveq1d ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) = ( 𝐴 + 𝐴 ) )
46 37 42 45 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
47 simpl ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → 𝐴 ∈ ℂ )
48 0cnd ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → 0 ∈ ℂ )
49 47 48 addcomd ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( 𝐴 + 0 ) = ( 0 + 𝐴 ) )
50 iffalse ( ¬ 𝜓 → if ( 𝜓 , 0 , 𝐴 ) = 𝐴 )
51 50 adantl ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , 0 , 𝐴 ) = 𝐴 )
52 iffalse ( ¬ 𝜓 → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = 0 )
53 52 adantl ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = 0 )
54 51 53 oveq12d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + 0 ) )
55 iffalse ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 0 ) = 0 )
56 55 adantl ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , 𝐴 , 0 ) = 0 )
57 56 oveq1d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) = ( 0 + 𝐴 ) )
58 49 54 57 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
59 46 58 pm2.61dan ( 𝐴 ∈ ℂ → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
60 59 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 𝐴 ) )
61 ifnot if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( 𝜓 , 0 , 𝐴 )
62 nbn2 ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑𝜓 ) ) )
63 62 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑𝜓 ) ) )
64 63 ifbid ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) )
65 61 64 eqtr3id ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 0 , 𝐴 ) = if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) )
66 biorf ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
67 66 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
68 67 ifbid ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
69 65 68 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
70 30 60 69 3eqtr2rd ( ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
71 23 70 pm2.61dan ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
72 hadrot ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ hadd ( 𝜑 , 𝜓 , 𝜒 ) )
73 had1 ( 𝜒 → ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑𝜓 ) ) )
74 72 73 bitr3id ( 𝜒 → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
75 74 adantl ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
76 75 ifbid ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) = if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) )
77 cad1 ( 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
78 77 adantl ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
79 78 ifbid ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
80 76 79 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
81 iftrue ( 𝜒 → if ( 𝜒 , 𝐴 , 0 ) = 𝐴 )
82 81 adantl ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → if ( 𝜒 , 𝐴 , 0 ) = 𝐴 )
83 82 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 𝐴 ) )
84 71 80 83 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )
85 19 adantl ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 𝐴 )
86 85 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
87 44 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) = ( 𝐴 + 𝐴 ) )
88 37 42 87 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
89 53 56 eqtr4d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
90 51 89 oveq12d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜓 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
91 88 90 pm2.61dan ( 𝐴 ∈ ℂ → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
92 91 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( 𝐴 + if ( 𝜓 , 𝐴 , 0 ) ) )
93 9 adantl ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
94 93 notbid ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( ¬ 𝜓 ↔ ¬ ( 𝜑𝜓 ) ) )
95 df-xor ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
96 94 95 bitr4di ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑𝜓 ) ) )
97 96 ifbid ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( ¬ 𝜓 , 𝐴 , 0 ) = if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) )
98 61 97 eqtr3id ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜓 , 0 , 𝐴 ) = if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) )
99 ibar ( 𝜑 → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
100 99 adantl ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( 𝜓 ↔ ( 𝜑𝜓 ) ) )
101 100 ifbid ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
102 98 101 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( 𝜓 , 0 , 𝐴 ) + if ( 𝜓 , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
103 86 92 102 3eqtr2rd ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ 𝜑 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
104 simplll ( ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) ∧ 𝜓 ) → 𝐴 ∈ ℂ )
105 0cnd ( ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) ∧ ¬ 𝜓 ) → 0 ∈ ℂ )
106 104 105 ifclda ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜓 , 𝐴 , 0 ) ∈ ℂ )
107 0cnd ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → 0 ∈ ℂ )
108 106 107 addcomd ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜓 , 𝐴 , 0 ) + 0 ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
109 62 adantl ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ 𝜓 ↔ ( 𝜑𝜓 ) ) )
110 109 con1bid ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ¬ ( 𝜑𝜓 ) ↔ 𝜓 ) )
111 95 110 syl5bb ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( ( 𝜑𝜓 ) ↔ 𝜓 ) )
112 111 ifbid ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) = if ( 𝜓 , 𝐴 , 0 ) )
113 simpr ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ¬ 𝜑 )
114 113 intnanrd ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ¬ ( 𝜑𝜓 ) )
115 iffalse ( ¬ ( 𝜑𝜓 ) → if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) = 0 )
116 114 115 syl ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) = 0 )
117 112 116 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜓 , 𝐴 , 0 ) + 0 ) )
118 24 adantl ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → if ( 𝜑 , 𝐴 , 0 ) = 0 )
119 118 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) = ( 0 + if ( 𝜓 , 𝐴 , 0 ) ) )
120 108 117 119 3eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) ∧ ¬ 𝜑 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
121 103 120 pm2.61dan ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
122 had0 ( ¬ 𝜒 → ( hadd ( 𝜒 , 𝜑 , 𝜓 ) ↔ ( 𝜑𝜓 ) ) )
123 72 122 bitr3id ( ¬ 𝜒 → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
124 123 adantl ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( hadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
125 124 ifbid ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) = if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) )
126 cad0 ( ¬ 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
127 126 adantl ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑𝜓 ) ) )
128 127 ifbid ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) = if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) )
129 125 128 oveq12d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( if ( ( 𝜑𝜓 ) , 𝐴 , 0 ) + if ( ( 𝜑𝜓 ) , ( 2 · 𝐴 ) , 0 ) ) )
130 iffalse ( ¬ 𝜒 → if ( 𝜒 , 𝐴 , 0 ) = 0 )
131 130 oveq2d ( ¬ 𝜒 → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 0 ) )
132 ifcl ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝜑 , 𝐴 , 0 ) ∈ ℂ )
133 1 132 mpan2 ( 𝐴 ∈ ℂ → if ( 𝜑 , 𝐴 , 0 ) ∈ ℂ )
134 133 3 addcld ( 𝐴 ∈ ℂ → ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) ∈ ℂ )
135 134 addid1d ( 𝐴 ∈ ℂ → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + 0 ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
136 131 135 sylan9eqr ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) = ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) )
137 121 129 136 3eqtr4d ( ( 𝐴 ∈ ℂ ∧ ¬ 𝜒 ) → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )
138 84 137 pm2.61dan ( 𝐴 ∈ ℂ → ( if ( hadd ( 𝜑 , 𝜓 , 𝜒 ) , 𝐴 , 0 ) + if ( cadd ( 𝜑 , 𝜓 , 𝜒 ) , ( 2 · 𝐴 ) , 0 ) ) = ( ( if ( 𝜑 , 𝐴 , 0 ) + if ( 𝜓 , 𝐴 , 0 ) ) + if ( 𝜒 , 𝐴 , 0 ) ) )