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 iftrue 
 |-  ( ( ph \/ ps ) -> if ( ( ph \/ ps ) , ( 2 x. A ) , 0 ) = ( 2 x. A ) )
15 13 14 syl 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> if ( ( ph \/ ps ) , ( 2 x. A ) , 0 ) = ( 2 x. A ) )
16 5 2timesd 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> ( 2 x. A ) = ( A + A ) )
17 15 16 eqtrd 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> if ( ( ph \/ ps ) , ( 2 x. A ) , 0 ) = ( A + A ) )
18 12 17 oveq12d 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> ( if ( ( ph <-> ps ) , A , 0 ) + if ( ( ph \/ ps ) , ( 2 x. A ) , 0 ) ) = ( if ( ps , A , 0 ) + ( A + A ) ) )
19 iftrue 
 |-  ( ph -> if ( ph , A , 0 ) = A )
20 19 adantl 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> if ( ph , A , 0 ) = A )
21 20 oveq1d 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) = ( A + if ( ps , A , 0 ) ) )
22 21 oveq1d 
 |-  ( ( ( A e. CC /\ ch ) /\ ph ) -> ( ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) + A ) = ( ( A + if ( ps , A , 0 ) ) + A ) )
23 8 18 22 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 ) )
24 iffalse 
 |-  ( -. ph -> if ( ph , A , 0 ) = 0 )
25 24 adantl 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> if ( ph , A , 0 ) = 0 )
26 25 oveq1d 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) = ( 0 + if ( ps , A , 0 ) ) )
27 3 ad2antrr 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> if ( ps , A , 0 ) e. CC )
28 27 addid2d 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( 0 + if ( ps , A , 0 ) ) = if ( ps , A , 0 ) )
29 26 28 eqtrd 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) = if ( ps , A , 0 ) )
30 29 oveq1d 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) + A ) = ( if ( ps , A , 0 ) + A ) )
31 2cnd 
 |-  ( A e. CC -> 2 e. CC )
32 id 
 |-  ( A e. CC -> A e. CC )
33 31 32 mulcld 
 |-  ( A e. CC -> ( 2 x. A ) e. CC )
34 33 addid2d 
 |-  ( A e. CC -> ( 0 + ( 2 x. A ) ) = ( 2 x. A ) )
35 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
36 34 35 eqtrd 
 |-  ( A e. CC -> ( 0 + ( 2 x. A ) ) = ( A + A ) )
37 36 adantr 
 |-  ( ( A e. CC /\ ps ) -> ( 0 + ( 2 x. A ) ) = ( A + A ) )
38 iftrue 
 |-  ( ps -> if ( ps , 0 , A ) = 0 )
39 38 adantl 
 |-  ( ( A e. CC /\ ps ) -> if ( ps , 0 , A ) = 0 )
40 iftrue 
 |-  ( ps -> if ( ps , ( 2 x. A ) , 0 ) = ( 2 x. A ) )
41 40 adantl 
 |-  ( ( A e. CC /\ ps ) -> if ( ps , ( 2 x. A ) , 0 ) = ( 2 x. A ) )
42 39 41 oveq12d 
 |-  ( ( A e. CC /\ ps ) -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( 0 + ( 2 x. A ) ) )
43 iftrue 
 |-  ( ps -> if ( ps , A , 0 ) = A )
44 43 adantl 
 |-  ( ( A e. CC /\ ps ) -> if ( ps , A , 0 ) = A )
45 44 oveq1d 
 |-  ( ( A e. CC /\ ps ) -> ( if ( ps , A , 0 ) + A ) = ( A + A ) )
46 37 42 45 3eqtr4d 
 |-  ( ( A e. CC /\ ps ) -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( if ( ps , A , 0 ) + A ) )
47 simpl 
 |-  ( ( A e. CC /\ -. ps ) -> A e. CC )
48 0cnd 
 |-  ( ( A e. CC /\ -. ps ) -> 0 e. CC )
49 47 48 addcomd 
 |-  ( ( A e. CC /\ -. ps ) -> ( A + 0 ) = ( 0 + A ) )
50 iffalse 
 |-  ( -. ps -> if ( ps , 0 , A ) = A )
51 50 adantl 
 |-  ( ( A e. CC /\ -. ps ) -> if ( ps , 0 , A ) = A )
52 iffalse 
 |-  ( -. ps -> if ( ps , ( 2 x. A ) , 0 ) = 0 )
53 52 adantl 
 |-  ( ( A e. CC /\ -. ps ) -> if ( ps , ( 2 x. A ) , 0 ) = 0 )
54 51 53 oveq12d 
 |-  ( ( A e. CC /\ -. ps ) -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( A + 0 ) )
55 iffalse 
 |-  ( -. ps -> if ( ps , A , 0 ) = 0 )
56 55 adantl 
 |-  ( ( A e. CC /\ -. ps ) -> if ( ps , A , 0 ) = 0 )
57 56 oveq1d 
 |-  ( ( A e. CC /\ -. ps ) -> ( if ( ps , A , 0 ) + A ) = ( 0 + A ) )
58 49 54 57 3eqtr4d 
 |-  ( ( A e. CC /\ -. ps ) -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( if ( ps , A , 0 ) + A ) )
59 46 58 pm2.61dan 
 |-  ( A e. CC -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( if ( ps , A , 0 ) + A ) )
60 59 ad2antrr 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( if ( ps , A , 0 ) + A ) )
61 ifnot 
 |-  if ( -. ps , A , 0 ) = if ( ps , 0 , A )
62 nbn2 
 |-  ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) )
63 62 adantl 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( -. ps <-> ( ph <-> ps ) ) )
64 63 ifbid 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> if ( -. ps , A , 0 ) = if ( ( ph <-> ps ) , A , 0 ) )
65 61 64 eqtr3id 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> if ( ps , 0 , A ) = if ( ( ph <-> ps ) , A , 0 ) )
66 biorf 
 |-  ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
67 66 adantl 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> ( ps <-> ( ph \/ ps ) ) )
68 67 ifbid 
 |-  ( ( ( A e. CC /\ ch ) /\ -. ph ) -> if ( ps , ( 2 x. A ) , 0 ) = if ( ( ph \/ ps ) , ( 2 x. A ) , 0 ) )
69 65 68 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 ) ) )
70 30 60 69 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 ) )
71 23 70 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 ) )
72 hadrot 
 |-  ( hadd ( ch , ph , ps ) <-> hadd ( ph , ps , ch ) )
73 had1 
 |-  ( ch -> ( hadd ( ch , ph , ps ) <-> ( ph <-> ps ) ) )
74 72 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 71 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 19 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 44 oveq2d 
 |-  ( ( A e. CC /\ ps ) -> ( A + if ( ps , A , 0 ) ) = ( A + A ) )
88 37 42 87 3eqtr4d 
 |-  ( ( A e. CC /\ ps ) -> ( if ( ps , 0 , A ) + if ( ps , ( 2 x. A ) , 0 ) ) = ( A + if ( ps , A , 0 ) ) )
89 53 56 eqtr4d 
 |-  ( ( A e. CC /\ -. ps ) -> if ( ps , ( 2 x. A ) , 0 ) = if ( ps , A , 0 ) )
90 51 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 61 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 62 adantl 
 |-  ( ( ( A e. CC /\ -. ch ) /\ -. ph ) -> ( -. ps <-> ( ph <-> ps ) ) )
110 109 con1bid 
 |-  ( ( ( A e. CC /\ -. ch ) /\ -. ph ) -> ( -. ( ph <-> ps ) <-> ps ) )
111 95 110 syl5bb 
 |-  ( ( ( 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 iffalse 
 |-  ( -. ( ph /\ ps ) -> if ( ( ph /\ ps ) , ( 2 x. A ) , 0 ) = 0 )
116 114 115 syl 
 |-  ( ( ( A e. CC /\ -. ch ) /\ -. ph ) -> if ( ( ph /\ ps ) , ( 2 x. A ) , 0 ) = 0 )
117 112 116 oveq12d 
 |-  ( ( ( A e. CC /\ -. ch ) /\ -. ph ) -> ( if ( ( ph \/_ ps ) , A , 0 ) + if ( ( ph /\ ps ) , ( 2 x. A ) , 0 ) ) = ( if ( ps , A , 0 ) + 0 ) )
118 24 adantl 
 |-  ( ( ( A e. CC /\ -. ch ) /\ -. ph ) -> if ( ph , A , 0 ) = 0 )
119 118 oveq1d 
 |-  ( ( ( A e. CC /\ -. ch ) /\ -. ph ) -> ( if ( ph , A , 0 ) + if ( ps , A , 0 ) ) = ( 0 + if ( ps , A , 0 ) ) )
120 108 117 119 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 ) ) )
121 103 120 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 ) ) )
122 had0 
 |-  ( -. ch -> ( hadd ( ch , ph , ps ) <-> ( ph \/_ ps ) ) )
123 72 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 addid1d 
 |-  ( 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 121 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 ) ) )