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 ⊢A∈ℂ→ifhaddφψχA0+ifcaddφψχ2⁢A0=ifφA0+ifψA0+ifχA0

Proof

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