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 iftrue ⊢ φ ∨ ψ → if φ ∨ ψ 2 ⁢ A 0 = 2 ⁢ A
15 13 14 syl ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ ∨ ψ 2 ⁢ A 0 = 2 ⁢ A
16 5 2timesd ⊢ A ∈ ℂ ∧ χ ∧ φ → 2 ⁢ A = A + A
17 15 16 eqtrd ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ ∨ ψ 2 ⁢ A 0 = A + A
18 12 17 oveq12d ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ ↔ ψ A 0 + if φ ∨ ψ 2 ⁢ A 0 = if ψ A 0 + A + A
19 iftrue ⊢ φ → if φ A 0 = A
20 19 adantl ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ A 0 = A
21 20 oveq1d ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ A 0 + if ψ A 0 = A + if ψ A 0
22 21 oveq1d ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ A 0 + if ψ A 0 + A = A + if ψ A 0 + A
23 8 18 22 3eqtr4d ⊢ A ∈ ℂ ∧ χ ∧ φ → if φ ↔ ψ A 0 + if φ ∨ ψ 2 ⁢ A 0 = if φ A 0 + if ψ A 0 + A
24 iffalse ⊢ ¬ φ → if φ A 0 = 0
25 24 adantl ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if φ A 0 = 0
26 25 oveq1d ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if φ A 0 + if ψ A 0 = 0 + if ψ A 0
27 3 ad2antrr ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if ψ A 0 ∈ ℂ
28 27 addid2d ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → 0 + if ψ A 0 = if ψ A 0
29 26 28 eqtrd ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if φ A 0 + if ψ A 0 = if ψ A 0
30 29 oveq1d ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if φ A 0 + if ψ A 0 + A = if ψ A 0 + A
31 2cnd ⊢ A ∈ ℂ → 2 ∈ ℂ
32 id ⊢ A ∈ ℂ → A ∈ ℂ
33 31 32 mulcld ⊢ A ∈ ℂ → 2 ⁢ A ∈ ℂ
34 33 addid2d ⊢ 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 ψ 0 A = 0
39 38 adantl ⊢ A ∈ ℂ ∧ ψ → if ψ 0 A = 0
40 iftrue ⊢ ψ → if ψ 2 ⁢ A 0 = 2 ⁢ A
41 40 adantl ⊢ A ∈ ℂ ∧ ψ → if ψ 2 ⁢ A 0 = 2 ⁢ A
42 39 41 oveq12d ⊢ A ∈ ℂ ∧ ψ → if ψ 0 A + if ψ 2 ⁢ A 0 = 0 + 2 ⁢ A
43 iftrue ⊢ ψ → if ψ A 0 = A
44 43 adantl ⊢ A ∈ ℂ ∧ ψ → if ψ A 0 = A
45 44 oveq1d ⊢ A ∈ ℂ ∧ ψ → if ψ A 0 + A = A + A
46 37 42 45 3eqtr4d ⊢ A ∈ ℂ ∧ ψ → if ψ 0 A + if ψ 2 ⁢ A 0 = if ψ A 0 + A
47 simpl ⊢ A ∈ ℂ ∧ ¬ ψ → A ∈ ℂ
48 0cnd ⊢ A ∈ ℂ ∧ ¬ ψ → 0 ∈ ℂ
49 47 48 addcomd ⊢ A ∈ ℂ ∧ ¬ ψ → A + 0 = 0 + A
50 iffalse ⊢ ¬ ψ → if ψ 0 A = A
51 50 adantl ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ 0 A = A
52 iffalse ⊢ ¬ ψ → if ψ 2 ⁢ A 0 = 0
53 52 adantl ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ 2 ⁢ A 0 = 0
54 51 53 oveq12d ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ 0 A + if ψ 2 ⁢ A 0 = A + 0
55 iffalse ⊢ ¬ ψ → if ψ A 0 = 0
56 55 adantl ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ A 0 = 0
57 56 oveq1d ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ A 0 + A = 0 + A
58 49 54 57 3eqtr4d ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ 0 A + if ψ 2 ⁢ A 0 = if ψ A 0 + A
59 46 58 pm2.61dan ⊢ A ∈ ℂ → if ψ 0 A + if ψ 2 ⁢ A 0 = if ψ A 0 + A
60 59 ad2antrr ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if ψ 0 A + if ψ 2 ⁢ A 0 = if ψ A 0 + A
61 ifnot ⊢ if ¬ ψ A 0 = if ψ 0 A
62 nbn2 ⊢ ¬ φ → ¬ ψ ↔ φ ↔ ψ
63 62 adantl ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → ¬ ψ ↔ φ ↔ ψ
64 63 ifbid ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if ¬ ψ A 0 = if φ ↔ ψ A 0
65 61 64 eqtr3id ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if ψ 0 A = if φ ↔ ψ A 0
66 biorf ⊢ ¬ φ → ψ ↔ φ ∨ ψ
67 66 adantl ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → ψ ↔ φ ∨ ψ
68 67 ifbid ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if ψ 2 ⁢ A 0 = if φ ∨ ψ 2 ⁢ A 0
69 65 68 oveq12d ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if ψ 0 A + if ψ 2 ⁢ A 0 = if φ ↔ ψ A 0 + if φ ∨ ψ 2 ⁢ A 0
70 30 60 69 3eqtr2rd ⊢ A ∈ ℂ ∧ χ ∧ ¬ φ → if φ ↔ ψ A 0 + if φ ∨ ψ 2 ⁢ A 0 = if φ A 0 + if ψ A 0 + A
71 23 70 pm2.61dan ⊢ A ∈ ℂ ∧ χ → if φ ↔ ψ A 0 + if φ ∨ ψ 2 ⁢ A 0 = if φ A 0 + if ψ A 0 + A
72 hadrot ⊢ hadd χ φ ψ ↔ hadd φ ψ χ
73 had1 ⊢ χ → hadd χ φ ψ ↔ φ ↔ ψ
74 72 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 71 80 83 3eqtr4d ⊢ A ∈ ℂ ∧ χ → if hadd φ ψ χ A 0 + if cadd φ ψ χ 2 ⁢ A 0 = if φ A 0 + if ψ A 0 + if χ A 0
85 19 adantl ⊢ A ∈ ℂ ∧ ¬ χ ∧ φ → if φ A 0 = A
86 85 oveq1d ⊢ A ∈ ℂ ∧ ¬ χ ∧ φ → if φ A 0 + if ψ A 0 = A + if ψ A 0
87 44 oveq2d ⊢ A ∈ ℂ ∧ ψ → A + if ψ A 0 = A + A
88 37 42 87 3eqtr4d ⊢ A ∈ ℂ ∧ ψ → if ψ 0 A + if ψ 2 ⁢ A 0 = A + if ψ A 0
89 53 56 eqtr4d ⊢ A ∈ ℂ ∧ ¬ ψ → if ψ 2 ⁢ A 0 = if ψ A 0
90 51 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 61 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 62 adantl ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → ¬ ψ ↔ φ ↔ ψ
110 109 con1bid ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → ¬ φ ↔ ψ ↔ ψ
111 95 110 syl5bb ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → φ ⊻ ψ ↔ ψ
112 111 ifbid ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → if φ ⊻ ψ A 0 = if ψ A 0
113 simpr ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → ¬ φ
114 113 intnanrd ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → ¬ φ ∧ ψ
115 iffalse ⊢ ¬ φ ∧ ψ → if φ ∧ ψ 2 ⁢ A 0 = 0
116 114 115 syl ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → if φ ∧ ψ 2 ⁢ A 0 = 0
117 112 116 oveq12d ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → if φ ⊻ ψ A 0 + if φ ∧ ψ 2 ⁢ A 0 = if ψ A 0 + 0
118 24 adantl ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → if φ A 0 = 0
119 118 oveq1d ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → if φ A 0 + if ψ A 0 = 0 + if ψ A 0
120 108 117 119 3eqtr4d ⊢ A ∈ ℂ ∧ ¬ χ ∧ ¬ φ → if φ ⊻ ψ A 0 + if φ ∧ ψ 2 ⁢ A 0 = if φ A 0 + if ψ A 0
121 103 120 pm2.61dan ⊢ A ∈ ℂ ∧ ¬ χ → if φ ⊻ ψ A 0 + if φ ∧ ψ 2 ⁢ A 0 = if φ A 0 + if ψ A 0
122 had0 ⊢ ¬ χ → hadd χ φ ψ ↔ φ ⊻ ψ
123 72 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 addid1d ⊢ 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 121 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