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 ∈ ℂ → if hadd φ ψ χ A 0 + if cadd φ ψ χ 2 ⁢ A 0 = if φ A 0 + if ψ A 0 + if χ A 0

Proof

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