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

Theorem sadadd2lem2 13645
Description: The core of the proof of sadadd2 13655. 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 9377 . . . . . . . . 9  |-  0  e.  CC
2 ifcl 3830 . . . . . . . . 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 9590 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
75, 4, 5addassd 9407 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
)  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
86, 7eqtr4d 2477 . . . . 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 3810 . . . . . 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 3796 . . . . . . . 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 10566 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( 2  x.  A )  =  ( A  +  A ) )
1816, 17eqtrd 2474 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( A  +  A ) )
1912, 18oveq12d 6108 . . . . 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 3796 . . . . . . . 8  |-  ( ph  ->  if ( ph ,  A ,  0 )  =  A )
2120adantl 466 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
2221oveq1d 6105 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
2322oveq1d 6105 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
) )
248, 19, 233eqtr4d 2484 . . . 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 3798 . . . . . . . . 9  |-  ( -. 
ph  ->  if ( ph ,  A ,  0 )  =  0 )
2625adantl 466 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
2726oveq1d 6105 . . . . . . 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 9569 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( 0  +  if ( ps ,  A ,  0 ) )  =  if ( ps ,  A ,  0 ) )
3027, 29eqtrd 2474 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  if ( ps ,  A ,  0 ) )
3130oveq1d 6105 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( if ( ps ,  A , 
0 )  +  A
) )
32 2cnd 10393 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  2  e.  CC )
33 id 22 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  A  e.  CC )
3432, 33mulcld 9405 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
2  x.  A )  e.  CC )
3534addid2d 9569 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( 2  x.  A ) )
36 2times 10439 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
3735, 36eqtrd 2474 . . . . . . . . 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 3796 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
0 ,  A )  =  0 )
4039adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  0 ,  A )  =  0 )
41 iftrue 3796 . . . . . . . . . 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 6108 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( 0  +  ( 2  x.  A ) ) )
44 iftrue 3796 . . . . . . . . . 10  |-  ( ps 
->  if ( ps ,  A ,  0 )  =  A )
4544adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  A , 
0 )  =  A )
4645oveq1d 6105 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( A  +  A ) )
4738, 43, 463eqtr4d 2484 . . . . . . 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 9378 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  0  e.  CC )
5048, 49addcomd 9570 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( A  +  0 )  =  ( 0  +  A ) )
51 iffalse 3798 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  0 ,  A
)  =  A )
5251adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  0 ,  A )  =  A )
53 iffalse 3798 . . . . . . . . . 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 6108 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  0 ) )
56 iffalse 3798 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  A ,  0 )  =  0 )
5756adantl 466 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  A , 
0 )  =  0 )
5857oveq1d 6105 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( 0  +  A ) )
5950, 55, 583eqtr4d 2484 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6047, 59pm2.61dan 789 . . . . . 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 3833 . . . . . . 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 3810 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( -.  ps ,  A , 
0 )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
6662, 65syl5eqr 2488 . . . . . 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 3810 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
7066, 69oveq12d 6108 . . . . 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 2481 . . . 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 789 . . 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 1431 . . . . . . 7  |-  (hadd ( ch ,  ph ,  ps )  <-> hadd ( ph ,  ps ,  ch ) )
74 had1 1444 . . . . . . 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 3810 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  <->  ps ) ,  A , 
0 ) )
78 cad1 1440 . . . . . 6  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
7978adantl 466 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (cadd (
ph ,  ps ,  ch )  <->  ( ph  \/  ps ) ) )
8079ifbid 3810 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
8177, 80oveq12d 6108 . . 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 3796 . . . . 5  |-  ( ch 
->  if ( ch ,  A ,  0 )  =  A )
8382adantl 466 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if ( ch ,  A , 
0 )  =  A )
8483oveq2d 6106 . . 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 2484 . 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 6105 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
8845oveq2d 6106 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( A  +  if ( ps ,  A ,  0 ) )  =  ( A  +  A ) )
8938, 43, 883eqtr4d 2484 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9054, 57eqtr4d 2477 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ps ,  A ,  0 ) )
9152, 90oveq12d 6108 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9289, 91pm2.61dan 789 . . . . . 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 1351 . . . . . . . . 9  |-  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
9795, 96syl6bbr 263 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  (
ph  \/_  ps )
) )
9897ifbid 3810 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( -. 
ps ,  A , 
0 )  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
9962, 98syl5eqr 2488 . . . . . 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 3810 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )
10399, 102oveq12d 6108 . . . . 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 2481 . . . 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 757 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  ps )  ->  A  e.  CC )
106 0cnd 9378 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  -.  ps )  -> 
0  e.  CC )
107105, 106ifclda 3820 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
108 0cnd 9378 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  0  e.  CC )
109107, 108addcomd 9570 . . . . 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 3810 . . . . . 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 908 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ( ph  /\  ps ) )
116 iffalse 3798 . . . . . . 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 6108 . . . . 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 6105 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
121109, 118, 1203eqtr4d 2484 . . . 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 789 . . 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 1445 . . . . . . 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 3810 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  \/_ 
ps ) ,  A ,  0 ) )
127 cad0 1442 . . . . . 6  |-  ( -. 
ch  ->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  /\  ps )
) )
128127adantl 466 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (cadd ( ph ,  ps ,  ch )  <->  ( ph  /\  ps ) ) )
129128ifbid 3810 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\ 
ps ) ,  ( 2  x.  A ) ,  0 ) )
130126, 129oveq12d 6108 . . 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 3798 . . . . 5  |-  ( -. 
ch  ->  if ( ch ,  A ,  0 )  =  0 )
132131oveq2d 6106 . . . 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 3830 . . . . . . 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 9404 . . . . 5  |-  ( A  e.  CC  ->  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  e.  CC )
136135addid1d 9568 . . . 4  |-  ( A  e.  CC  ->  (
( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  0 )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
137132, 136sylan9eqr 2496 . . 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 2484 . 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 789 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 1350    = wceq 1369  haddwhad 1419  caddwcad 1420    e. wcel 1756   ifcif 3790  (class class class)co 6090   CCcc 9279   0cc0 9281    + caddc 9284    x. cmul 9286   2c2 10370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371  ax-resscn 9338  ax-1cn 9339  ax-icn 9340  ax-addcl 9341  ax-addrcl 9342  ax-mulcl 9343  ax-mulrcl 9344  ax-mulcom 9345  ax-addass 9346  ax-mulass 9347  ax-distr 9348  ax-i2m1 9349  ax-1ne0 9350  ax-1rid 9351  ax-rnegex 9352  ax-rrecex 9353  ax-cnre 9354  ax-pre-lttri 9355  ax-pre-lttrn 9356  ax-pre-ltadd 9357
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-xor 1351  df-tru 1372  df-had 1421  df-cad 1422  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-mpt 4351  df-id 4635  df-po 4640  df-so 4641  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6093  df-er 7100  df-en 7310  df-dom 7311  df-sdom 7312  df-pnf 9419  df-mnf 9420  df-ltxr 9422  df-2 10379
This theorem is referenced by:  sadadd2lem  13654
  Copyright terms: Public domain W3C validator