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 e. CC -> ( if ( hadd ( ph , ps , ch ) , A , 0 ) + if ( cadd ( ph , ps , ch ) , ( 2 x. A ) , 0 ) ) = ( ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) + if ( ch , A , 0 ) ) )

Proof

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