MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadadd2lem2 Unicode version

Theorem sadadd2lem2 12889
Description: The core of the proof of sadadd2 12899. 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.)
Assertion
Ref Expression
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 of Theorem sadadd2lem2
StepHypRef Expression
1 0cn 9017 . . . . . . . . 9  |-  0  e.  CC
2 ifcl 3718 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ps ,  A ,  0 )  e.  CC )
31, 2mpan2 653 . . . . . . . 8  |-  ( A  e.  CC  ->  if ( ps ,  A , 
0 )  e.  CC )
43ad2antrr 707 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ps ,  A ,  0 )  e.  CC )
5 simpll 731 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  A  e.  CC )
64, 5, 5add12d 9219 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
75, 4, 5addassd 9043 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
)  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
86, 7eqtr4d 2422 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( ( A  +  if ( ps ,  A , 
0 ) )  +  A ) )
9 pm5.501 331 . . . . . . . . 9  |-  ( ph  ->  ( ps  <->  ( ph  <->  ps ) ) )
109adantl 453 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
1110bicomd 193 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( ph  <->  ps )  <->  ps ) )
1211ifbid 3700 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph 
<->  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
13 simpr 448 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ph )
1413orcd 382 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ph  \/  ps ) )
15 iftrue 3688 . . . . . . . 8  |-  ( (
ph  \/  ps )  ->  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A
) )
1614, 15syl 16 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
1752timesd 10142 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( 2  x.  A )  =  ( A  +  A ) )
1816, 17eqtrd 2419 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( A  +  A ) )
1912, 18oveq12d 6038 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ( ph  <->  ps ) ,  A ,  0 )  +  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  ( A  +  A ) ) )
20 iftrue 3688 . . . . . . . 8  |-  ( ph  ->  if ( ph ,  A ,  0 )  =  A )
2120adantl 453 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
2221oveq1d 6035 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
2322oveq1d 6035 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
) )
248, 19, 233eqtr4d 2429 . . . 4  |-  ( ( ( 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
) )
25 iffalse 3689 . . . . . . . . 9  |-  ( -. 
ph  ->  if ( ph ,  A ,  0 )  =  0 )
2625adantl 453 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
2726oveq1d 6035 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
283ad2antrr 707 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
2928addid2d 9199 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( 0  +  if ( ps ,  A ,  0 ) )  =  if ( ps ,  A ,  0 ) )
3027, 29eqtrd 2419 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  if ( ps ,  A ,  0 ) )
3130oveq1d 6035 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( if ( ps ,  A , 
0 )  +  A
) )
32 2cn 10002 . . . . . . . . . . . . 13  |-  2  e.  CC
3332a1i 11 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  2  e.  CC )
34 id 20 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  A  e.  CC )
3533, 34mulcld 9041 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
2  x.  A )  e.  CC )
3635addid2d 9199 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( 2  x.  A ) )
37 2times 10031 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
3836, 37eqtrd 2419 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( A  +  A ) )
3938adantr 452 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( 0  +  ( 2  x.  A ) )  =  ( A  +  A
) )
40 iftrue 3688 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
0 ,  A )  =  0 )
4140adantl 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  0 ,  A )  =  0 )
42 iftrue 3688 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
( 2  x.  A
) ,  0 )  =  ( 2  x.  A ) )
4342adantl 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
4441, 43oveq12d 6038 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( 0  +  ( 2  x.  A ) ) )
45 iftrue 3688 . . . . . . . . . 10  |-  ( ps 
->  if ( ps ,  A ,  0 )  =  A )
4645adantl 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  A , 
0 )  =  A )
4746oveq1d 6035 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( A  +  A ) )
4839, 44, 473eqtr4d 2429 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
49 simpl 444 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  A  e.  CC )
501a1i 11 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  0  e.  CC )
5149, 50addcomd 9200 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( A  +  0 )  =  ( 0  +  A ) )
52 iffalse 3689 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  0 ,  A
)  =  A )
5352adantl 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  0 ,  A )  =  A )
54 iffalse 3689 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5554adantl 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5653, 55oveq12d 6038 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  0 ) )
57 iffalse 3689 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  A ,  0 )  =  0 )
5857adantl 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  A , 
0 )  =  0 )
5958oveq1d 6035 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( 0  +  A ) )
6051, 56, 593eqtr4d 2429 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6148, 60pm2.61dan 767 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6261ad2antrr 707 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
63 ifnot 3720 . . . . . . 7  |-  if ( -.  ps ,  A ,  0 )  =  if ( ps , 
0 ,  A )
64 nbn2 335 . . . . . . . . 9  |-  ( -. 
ph  ->  ( -.  ps  <->  (
ph 
<->  ps ) ) )
6564adantl 453 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
6665ifbid 3700 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( -.  ps ,  A , 
0 )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
6763, 66syl5eqr 2433 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  0 ,  A )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
68 biorf 395 . . . . . . . 8  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
6968adantl 453 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ps  <->  (
ph  \/  ps )
) )
7069ifbid 3700 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
7167, 70oveq12d 6038 . . . . 5  |-  ( ( ( 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 ) ) )
7231, 62, 713eqtr2rd 2426 . . . 4  |-  ( ( ( 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
) )
7324, 72pm2.61dan 767 . . 3  |-  ( ( 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
) )
74 hadrot 1396 . . . . . . 7  |-  (hadd ( ch ,  ph ,  ps )  <-> hadd ( ph ,  ps ,  ch ) )
75 had1 1408 . . . . . . 7  |-  ( ch 
->  (hadd ( ch ,  ph ,  ps )  <->  (
ph 
<->  ps ) ) )
7674, 75syl5bbr 251 . . . . . 6  |-  ( ch 
->  (hadd ( ph ,  ps ,  ch )  <->  (
ph 
<->  ps ) ) )
7776adantl 453 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (hadd (
ph ,  ps ,  ch )  <->  ( ph  <->  ps )
) )
7877ifbid 3700 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  <->  ps ) ,  A , 
0 ) )
79 cad1 1404 . . . . . 6  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
8079adantl 453 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (cadd (
ph ,  ps ,  ch )  <->  ( ph  \/  ps ) ) )
8180ifbid 3700 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
8278, 81oveq12d 6038 . . 3  |-  ( ( 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 ) ) )
83 iftrue 3688 . . . . 5  |-  ( ch 
->  if ( ch ,  A ,  0 )  =  A )
8483adantl 453 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if ( ch ,  A , 
0 )  =  A )
8584oveq2d 6036 . . 3  |-  ( ( 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 ) )
8673, 82, 853eqtr4d 2429 . 2  |-  ( ( 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 ) ) )
8720adantl 453 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
8887oveq1d 6035 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
8946oveq2d 6036 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( A  +  if ( ps ,  A ,  0 ) )  =  ( A  +  A ) )
9039, 44, 893eqtr4d 2429 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9155, 58eqtr4d 2422 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ps ,  A ,  0 ) )
9253, 91oveq12d 6038 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9390, 92pm2.61dan 767 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9493ad2antrr 707 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
959adantl 453 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
9695notbid 286 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  -.  ( ph  <->  ps )
) )
97 df-xor 1311 . . . . . . . . 9  |-  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
9896, 97syl6bbr 255 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  (
ph  \/_  ps )
) )
9998ifbid 3700 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( -. 
ps ,  A , 
0 )  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
10063, 99syl5eqr 2433 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  0 ,  A
)  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
101 ibar 491 . . . . . . . 8  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
102101adantl 453 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
103102ifbid 3700 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )
104100, 103oveq12d 6038 . . . . 5  |-  ( ( ( 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 ) ) )
10588, 94, 1043eqtr2rd 2426 . . . 4  |-  ( ( ( 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 ) ) )
106 simplll 735 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  ps )  ->  A  e.  CC )
1071a1i 11 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  -.  ps )  -> 
0  e.  CC )
108106, 107ifclda 3709 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
1091a1i 11 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  0  e.  CC )
110108, 109addcomd 9200 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ps ,  A , 
0 )  +  0 )  =  ( 0  +  if ( ps ,  A ,  0 ) ) )
11164adantl 453 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
112111con1bid 321 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ( ph  <->  ps )  <->  ps )
)
11397, 112syl5bb 249 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( ( ph  \/_  ps )  <->  ps )
)
114113ifbid 3700 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  \/_  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
115 simpr 448 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ph )
116115intnanrd 884 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ( ph  /\  ps ) )
117 iffalse 3689 . . . . . . 7  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
118116, 117syl 16 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
119114, 118oveq12d 6038 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ( ph  \/_  ps ) ,  A , 
0 )  +  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  0 ) )
12025adantl 453 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
121120oveq1d 6035 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
122110, 119, 1213eqtr4d 2429 . . . 4  |-  ( ( ( 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 ) ) )
123105, 122pm2.61dan 767 . . 3  |-  ( ( A  e.  CC  /\  -.  ch )  ->  ( if ( ( ph  \/_  ps ) ,  A , 
0 )  +  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
124 had0 1409 . . . . . . 7  |-  ( -. 
ch  ->  (hadd ( ch ,  ph ,  ps ) 
<->  ( ph  \/_  ps ) ) )
12574, 124syl5bbr 251 . . . . . 6  |-  ( -. 
ch  ->  (hadd ( ph ,  ps ,  ch )  <->  (
ph  \/_  ps )
) )
126125adantl 453 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (hadd ( ph ,  ps ,  ch )  <->  ( ph  \/_  ps ) ) )
127126ifbid 3700 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  \/_ 
ps ) ,  A ,  0 ) )
128 cad0 1406 . . . . . 6  |-  ( -. 
ch  ->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  /\  ps )
) )
129128adantl 453 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (cadd ( ph ,  ps ,  ch )  <->  ( ph  /\  ps ) ) )
130129ifbid 3700 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\ 
ps ) ,  ( 2  x.  A ) ,  0 ) )
131127, 130oveq12d 6038 . . 3  |-  ( ( 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 ) ) )
132 iffalse 3689 . . . . 5  |-  ( -. 
ch  ->  if ( ch ,  A ,  0 )  =  0 )
133132oveq2d 6036 . . . 4  |-  ( -. 
ch  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  if ( ch ,  A , 
0 ) )  =  ( ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  +  0 ) )
134 ifcl 3718 . . . . . . 7  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ph ,  A ,  0 )  e.  CC )
1351, 134mpan2 653 . . . . . 6  |-  ( A  e.  CC  ->  if ( ph ,  A , 
0 )  e.  CC )
136135, 3addcld 9040 . . . . 5  |-  ( A  e.  CC  ->  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  e.  CC )
137136addid1d 9198 . . . 4  |-  ( A  e.  CC  ->  (
( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  0 )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
138133, 137sylan9eqr 2441 . . 3  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (
( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  if ( ch ,  A , 
0 ) )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
139123, 131, 1383eqtr4d 2429 . 2  |-  ( ( 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 ) ) )
14086, 139pm2.61dan 767 1  |-  ( 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 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    \/_ wxo 1310  haddwhad 1384  caddwcad 1385    = wceq 1649    e. wcel 1717   ifcif 3682  (class class class)co 6020   CCcc 8921   0cc0 8923    + caddc 8926    x. cmul 8928   2c2 9981
This theorem is referenced by:  sadadd2lem  12898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-xor 1311  df-tru 1325  df-had 1386  df-cad 1387  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-po 4444  df-so 4445  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-er 6841  df-en 7046  df-dom 7047  df-sdom 7048  df-pnf 9055  df-mnf 9056  df-ltxr 9058  df-2 9990
  Copyright terms: Public domain W3C validator