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

Theorem sadadd2lem2 14111
Description: The core of the proof of sadadd2 14121. 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 9605 . . . . . . . . 9  |-  0  e.  CC
2 ifcl 3986 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ps ,  A ,  0 )  e.  CC )
31, 2mpan2 671 . . . . . . . 8  |-  ( A  e.  CC  ->  if ( ps ,  A , 
0 )  e.  CC )
43ad2antrr 725 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ps ,  A ,  0 )  e.  CC )
5 simpll 753 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  A  e.  CC )
64, 5, 5add12d 9820 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
75, 4, 5addassd 9635 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
)  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
86, 7eqtr4d 2501 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( ( A  +  if ( ps ,  A , 
0 ) )  +  A ) )
9 pm5.501 341 . . . . . . . . 9  |-  ( ph  ->  ( ps  <->  ( ph  <->  ps ) ) )
109adantl 466 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
1110bicomd 201 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( ph  <->  ps )  <->  ps ) )
1211ifbid 3966 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph 
<->  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
13 simpr 461 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ph )
1413orcd 392 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ph  \/  ps ) )
15 iftrue 3950 . . . . . . . 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 10802 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( 2  x.  A )  =  ( A  +  A ) )
1816, 17eqtrd 2498 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( A  +  A ) )
1912, 18oveq12d 6314 . . . . 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 3950 . . . . . . . 8  |-  ( ph  ->  if ( ph ,  A ,  0 )  =  A )
2120adantl 466 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
2221oveq1d 6311 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
2322oveq1d 6311 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
) )
248, 19, 233eqtr4d 2508 . . . 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 3953 . . . . . . . . 9  |-  ( -. 
ph  ->  if ( ph ,  A ,  0 )  =  0 )
2625adantl 466 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
2726oveq1d 6311 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
283ad2antrr 725 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
2928addid2d 9798 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( 0  +  if ( ps ,  A ,  0 ) )  =  if ( ps ,  A ,  0 ) )
3027, 29eqtrd 2498 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  if ( ps ,  A ,  0 ) )
3130oveq1d 6311 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( if ( ps ,  A , 
0 )  +  A
) )
32 2cnd 10629 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  2  e.  CC )
33 id 22 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  A  e.  CC )
3432, 33mulcld 9633 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
2  x.  A )  e.  CC )
3534addid2d 9798 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( 2  x.  A ) )
36 2times 10675 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
3735, 36eqtrd 2498 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( A  +  A ) )
3837adantr 465 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( 0  +  ( 2  x.  A ) )  =  ( A  +  A
) )
39 iftrue 3950 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
0 ,  A )  =  0 )
4039adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  0 ,  A )  =  0 )
41 iftrue 3950 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
( 2  x.  A
) ,  0 )  =  ( 2  x.  A ) )
4241adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
4340, 42oveq12d 6314 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( 0  +  ( 2  x.  A ) ) )
44 iftrue 3950 . . . . . . . . . 10  |-  ( ps 
->  if ( ps ,  A ,  0 )  =  A )
4544adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  A , 
0 )  =  A )
4645oveq1d 6311 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( A  +  A ) )
4738, 43, 463eqtr4d 2508 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
48 simpl 457 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  A  e.  CC )
49 0cnd 9606 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  0  e.  CC )
5048, 49addcomd 9799 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( A  +  0 )  =  ( 0  +  A ) )
51 iffalse 3953 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  0 ,  A
)  =  A )
5251adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  0 ,  A )  =  A )
53 iffalse 3953 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5453adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5552, 54oveq12d 6314 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  0 ) )
56 iffalse 3953 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  A ,  0 )  =  0 )
5756adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  A , 
0 )  =  0 )
5857oveq1d 6311 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( 0  +  A ) )
5950, 55, 583eqtr4d 2508 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6047, 59pm2.61dan 791 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6160ad2antrr 725 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
62 ifnot 3989 . . . . . . 7  |-  if ( -.  ps ,  A ,  0 )  =  if ( ps , 
0 ,  A )
63 nbn2 345 . . . . . . . . 9  |-  ( -. 
ph  ->  ( -.  ps  <->  (
ph 
<->  ps ) ) )
6463adantl 466 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
6564ifbid 3966 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( -.  ps ,  A , 
0 )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
6662, 65syl5eqr 2512 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  0 ,  A )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
67 biorf 405 . . . . . . . 8  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
6867adantl 466 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ps  <->  (
ph  \/  ps )
) )
6968ifbid 3966 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
7066, 69oveq12d 6314 . . . . 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 ) ) )
7131, 61, 703eqtr2rd 2505 . . . 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
) )
7224, 71pm2.61dan 791 . . 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
) )
73 hadrot 1457 . . . . . . 7  |-  (hadd ( ch ,  ph ,  ps )  <-> hadd ( ph ,  ps ,  ch ) )
74 had1 1470 . . . . . . 7  |-  ( ch 
->  (hadd ( ch ,  ph ,  ps )  <->  (
ph 
<->  ps ) ) )
7573, 74syl5bbr 259 . . . . . 6  |-  ( ch 
->  (hadd ( ph ,  ps ,  ch )  <->  (
ph 
<->  ps ) ) )
7675adantl 466 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (hadd (
ph ,  ps ,  ch )  <->  ( ph  <->  ps )
) )
7776ifbid 3966 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  <->  ps ) ,  A , 
0 ) )
78 cad1 1465 . . . . . 6  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
7978adantl 466 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (cadd (
ph ,  ps ,  ch )  <->  ( ph  \/  ps ) ) )
8079ifbid 3966 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
8177, 80oveq12d 6314 . . 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 ) ) )
82 iftrue 3950 . . . . 5  |-  ( ch 
->  if ( ch ,  A ,  0 )  =  A )
8382adantl 466 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if ( ch ,  A , 
0 )  =  A )
8483oveq2d 6312 . . 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 ) )
8572, 81, 843eqtr4d 2508 . 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 ) ) )
8620adantl 466 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
8786oveq1d 6311 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
8845oveq2d 6312 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( A  +  if ( ps ,  A ,  0 ) )  =  ( A  +  A ) )
8938, 43, 883eqtr4d 2508 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9054, 57eqtr4d 2501 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ps ,  A ,  0 ) )
9152, 90oveq12d 6314 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9289, 91pm2.61dan 791 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9392ad2antrr 725 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
949adantl 466 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
9594notbid 294 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  -.  ( ph  <->  ps )
) )
96 df-xor 1364 . . . . . . . . 9  |-  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
9795, 96syl6bbr 263 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  (
ph  \/_  ps )
) )
9897ifbid 3966 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( -. 
ps ,  A , 
0 )  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
9962, 98syl5eqr 2512 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  0 ,  A
)  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
100 ibar 504 . . . . . . . 8  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
101100adantl 466 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
102101ifbid 3966 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )
10399, 102oveq12d 6314 . . . . 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 ) ) )
10487, 93, 1033eqtr2rd 2505 . . . 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 ) ) )
105 simplll 759 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  ps )  ->  A  e.  CC )
106 0cnd 9606 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  -.  ps )  -> 
0  e.  CC )
107105, 106ifclda 3976 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
108 0cnd 9606 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  0  e.  CC )
109107, 108addcomd 9799 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ps ,  A , 
0 )  +  0 )  =  ( 0  +  if ( ps ,  A ,  0 ) ) )
11063adantl 466 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
111110con1bid 330 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ( ph  <->  ps )  <->  ps )
)
11296, 111syl5bb 257 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( ( ph  \/_  ps )  <->  ps )
)
113112ifbid 3966 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  \/_  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
114 simpr 461 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ph )
115114intnanrd 917 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ( ph  /\  ps ) )
116 iffalse 3953 . . . . . . 7  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
117115, 116syl 16 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
118113, 117oveq12d 6314 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ( ph  \/_  ps ) ,  A , 
0 )  +  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  0 ) )
11925adantl 466 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
120119oveq1d 6311 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
121109, 118, 1203eqtr4d 2508 . . . 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 ) ) )
122104, 121pm2.61dan 791 . . 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 ) ) )
123 had0 1471 . . . . . . 7  |-  ( -. 
ch  ->  (hadd ( ch ,  ph ,  ps ) 
<->  ( ph  \/_  ps ) ) )
12473, 123syl5bbr 259 . . . . . 6  |-  ( -. 
ch  ->  (hadd ( ph ,  ps ,  ch )  <->  (
ph  \/_  ps )
) )
125124adantl 466 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (hadd ( ph ,  ps ,  ch )  <->  ( ph  \/_  ps ) ) )
126125ifbid 3966 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  \/_ 
ps ) ,  A ,  0 ) )
127 cad0 1467 . . . . . 6  |-  ( -. 
ch  ->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  /\  ps )
) )
128127adantl 466 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (cadd ( ph ,  ps ,  ch )  <->  ( ph  /\  ps ) ) )
129128ifbid 3966 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\ 
ps ) ,  ( 2  x.  A ) ,  0 ) )
130126, 129oveq12d 6314 . . 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 ) ) )
131 iffalse 3953 . . . . 5  |-  ( -. 
ch  ->  if ( ch ,  A ,  0 )  =  0 )
132131oveq2d 6312 . . . 4  |-  ( -. 
ch  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  if ( ch ,  A , 
0 ) )  =  ( ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  +  0 ) )
133 ifcl 3986 . . . . . . 7  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ph ,  A ,  0 )  e.  CC )
1341, 133mpan2 671 . . . . . 6  |-  ( A  e.  CC  ->  if ( ph ,  A , 
0 )  e.  CC )
135134, 3addcld 9632 . . . . 5  |-  ( A  e.  CC  ->  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  e.  CC )
136135addid1d 9797 . . . 4  |-  ( A  e.  CC  ->  (
( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  0 )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
137132, 136sylan9eqr 2520 . . 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 ) ) )
138122, 130, 1373eqtr4d 2508 . 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 ) ) )
13985, 138pm2.61dan 791 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    \/_ wxo 1363    = wceq 1395  haddwhad 1445  caddwcad 1446    e. wcel 1819   ifcif 3944  (class class class)co 6296   CCcc 9507   0cc0 9509    + caddc 9512    x. cmul 9514   2c2 10606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-xor 1364  df-tru 1398  df-had 1447  df-cad 1448  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-po 4809  df-so 4810  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ov 6299  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-pnf 9647  df-mnf 9648  df-ltxr 9650  df-2 10615
This theorem is referenced by:  sadadd2lem  14120
  Copyright terms: Public domain W3C validator