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

Theorem sadadd2lem2 14503
Description: The core of the proof of sadadd2 14513. 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 9653 . . . . . . . . 9  |-  0  e.  CC
2 ifcl 3914 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ps ,  A ,  0 )  e.  CC )
31, 2mpan2 685 . . . . . . . 8  |-  ( A  e.  CC  ->  if ( ps ,  A , 
0 )  e.  CC )
43ad2antrr 740 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ps ,  A ,  0 )  e.  CC )
5 simpll 768 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  A  e.  CC )
64, 5, 5add12d 9876 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
75, 4, 5addassd 9683 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
)  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
86, 7eqtr4d 2508 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( ( A  +  if ( ps ,  A , 
0 ) )  +  A ) )
9 pm5.501 348 . . . . . . . . 9  |-  ( ph  ->  ( ps  <->  ( ph  <->  ps ) ) )
109adantl 473 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
1110bicomd 206 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( ph  <->  ps )  <->  ps ) )
1211ifbid 3894 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph 
<->  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
13 simpr 468 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ph )
1413orcd 399 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ph  \/  ps ) )
15 iftrue 3878 . . . . . . . 8  |-  ( (
ph  \/  ps )  ->  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A
) )
1614, 15syl 17 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
1752timesd 10878 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( 2  x.  A )  =  ( A  +  A ) )
1816, 17eqtrd 2505 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( A  +  A ) )
1912, 18oveq12d 6326 . . . . 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 3878 . . . . . . . 8  |-  ( ph  ->  if ( ph ,  A ,  0 )  =  A )
2120adantl 473 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
2221oveq1d 6323 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
2322oveq1d 6323 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
) )
248, 19, 233eqtr4d 2515 . . . 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 3881 . . . . . . . . 9  |-  ( -. 
ph  ->  if ( ph ,  A ,  0 )  =  0 )
2625adantl 473 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
2726oveq1d 6323 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
283ad2antrr 740 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
2928addid2d 9852 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( 0  +  if ( ps ,  A ,  0 ) )  =  if ( ps ,  A ,  0 ) )
3027, 29eqtrd 2505 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  if ( ps ,  A ,  0 ) )
3130oveq1d 6323 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( if ( ps ,  A , 
0 )  +  A
) )
32 2cnd 10704 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  2  e.  CC )
33 id 22 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  A  e.  CC )
3432, 33mulcld 9681 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
2  x.  A )  e.  CC )
3534addid2d 9852 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( 2  x.  A ) )
36 2times 10751 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
3735, 36eqtrd 2505 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( A  +  A ) )
3837adantr 472 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( 0  +  ( 2  x.  A ) )  =  ( A  +  A
) )
39 iftrue 3878 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
0 ,  A )  =  0 )
4039adantl 473 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  0 ,  A )  =  0 )
41 iftrue 3878 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
( 2  x.  A
) ,  0 )  =  ( 2  x.  A ) )
4241adantl 473 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
4340, 42oveq12d 6326 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( 0  +  ( 2  x.  A ) ) )
44 iftrue 3878 . . . . . . . . . 10  |-  ( ps 
->  if ( ps ,  A ,  0 )  =  A )
4544adantl 473 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  A , 
0 )  =  A )
4645oveq1d 6323 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( A  +  A ) )
4738, 43, 463eqtr4d 2515 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
48 simpl 464 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  A  e.  CC )
49 0cnd 9654 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  0  e.  CC )
5048, 49addcomd 9853 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( A  +  0 )  =  ( 0  +  A ) )
51 iffalse 3881 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  0 ,  A
)  =  A )
5251adantl 473 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  0 ,  A )  =  A )
53 iffalse 3881 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5453adantl 473 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5552, 54oveq12d 6326 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  0 ) )
56 iffalse 3881 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  A ,  0 )  =  0 )
5756adantl 473 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  A , 
0 )  =  0 )
5857oveq1d 6323 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( 0  +  A ) )
5950, 55, 583eqtr4d 2515 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6047, 59pm2.61dan 808 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6160ad2antrr 740 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
62 ifnot 3917 . . . . . . 7  |-  if ( -.  ps ,  A ,  0 )  =  if ( ps , 
0 ,  A )
63 nbn2 352 . . . . . . . . 9  |-  ( -. 
ph  ->  ( -.  ps  <->  (
ph 
<->  ps ) ) )
6463adantl 473 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
6564ifbid 3894 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( -.  ps ,  A , 
0 )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
6662, 65syl5eqr 2519 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  0 ,  A )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
67 biorf 412 . . . . . . . 8  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
6867adantl 473 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ps  <->  (
ph  \/  ps )
) )
6968ifbid 3894 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
7066, 69oveq12d 6326 . . . . 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 2512 . . . 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 808 . . 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 1512 . . . . . . 7  |-  (hadd ( ch ,  ph ,  ps )  <-> hadd ( ph ,  ps ,  ch ) )
74 had1 1514 . . . . . . 7  |-  ( ch 
->  (hadd ( ch ,  ph ,  ps )  <->  (
ph 
<->  ps ) ) )
7573, 74syl5bbr 267 . . . . . 6  |-  ( ch 
->  (hadd ( ph ,  ps ,  ch )  <->  (
ph 
<->  ps ) ) )
7675adantl 473 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (hadd (
ph ,  ps ,  ch )  <->  ( ph  <->  ps )
) )
7776ifbid 3894 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  <->  ps ) ,  A , 
0 ) )
78 cad1 1527 . . . . . 6  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
7978adantl 473 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (cadd (
ph ,  ps ,  ch )  <->  ( ph  \/  ps ) ) )
8079ifbid 3894 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
8177, 80oveq12d 6326 . . 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 3878 . . . . 5  |-  ( ch 
->  if ( ch ,  A ,  0 )  =  A )
8382adantl 473 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if ( ch ,  A , 
0 )  =  A )
8483oveq2d 6324 . . 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 2515 . 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 473 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
8786oveq1d 6323 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
8845oveq2d 6324 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( A  +  if ( ps ,  A ,  0 ) )  =  ( A  +  A ) )
8938, 43, 883eqtr4d 2515 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9054, 57eqtr4d 2508 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ps ,  A ,  0 ) )
9152, 90oveq12d 6326 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9289, 91pm2.61dan 808 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9392ad2antrr 740 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
949adantl 473 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
9594notbid 301 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  -.  ( ph  <->  ps )
) )
96 df-xor 1431 . . . . . . . . 9  |-  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
9795, 96syl6bbr 271 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  (
ph  \/_  ps )
) )
9897ifbid 3894 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( -. 
ps ,  A , 
0 )  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
9962, 98syl5eqr 2519 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  0 ,  A
)  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
100 ibar 512 . . . . . . . 8  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
101100adantl 473 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
102101ifbid 3894 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )
10399, 102oveq12d 6326 . . . . 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 2512 . . . 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 776 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  ps )  ->  A  e.  CC )
106 0cnd 9654 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  -.  ps )  -> 
0  e.  CC )
107105, 106ifclda 3904 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
108 0cnd 9654 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  0  e.  CC )
109107, 108addcomd 9853 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ps ,  A , 
0 )  +  0 )  =  ( 0  +  if ( ps ,  A ,  0 ) ) )
11063adantl 473 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
111110con1bid 337 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ( ph  <->  ps )  <->  ps )
)
11296, 111syl5bb 265 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( ( ph  \/_  ps )  <->  ps )
)
113112ifbid 3894 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  \/_  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
114 simpr 468 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ph )
115114intnanrd 931 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ( ph  /\  ps ) )
116 iffalse 3881 . . . . . . 7  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
117115, 116syl 17 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
118113, 117oveq12d 6326 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ( ph  \/_  ps ) ,  A , 
0 )  +  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  0 ) )
11925adantl 473 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
120119oveq1d 6323 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
121109, 118, 1203eqtr4d 2515 . . . 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 808 . . 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 1515 . . . . . . 7  |-  ( -. 
ch  ->  (hadd ( ch ,  ph ,  ps ) 
<->  ( ph  \/_  ps ) ) )
12473, 123syl5bbr 267 . . . . . 6  |-  ( -. 
ch  ->  (hadd ( ph ,  ps ,  ch )  <->  (
ph  \/_  ps )
) )
125124adantl 473 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (hadd ( ph ,  ps ,  ch )  <->  ( ph  \/_  ps ) ) )
126125ifbid 3894 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  \/_ 
ps ) ,  A ,  0 ) )
127 cad0 1528 . . . . . 6  |-  ( -. 
ch  ->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  /\  ps )
) )
128127adantl 473 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (cadd ( ph ,  ps ,  ch )  <->  ( ph  /\  ps ) ) )
129128ifbid 3894 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\ 
ps ) ,  ( 2  x.  A ) ,  0 ) )
130126, 129oveq12d 6326 . . 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 3881 . . . . 5  |-  ( -. 
ch  ->  if ( ch ,  A ,  0 )  =  0 )
132131oveq2d 6324 . . . 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 3914 . . . . . . 7  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ph ,  A ,  0 )  e.  CC )
1341, 133mpan2 685 . . . . . 6  |-  ( A  e.  CC  ->  if ( ph ,  A , 
0 )  e.  CC )
135134, 3addcld 9680 . . . . 5  |-  ( A  e.  CC  ->  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  e.  CC )
136135addid1d 9851 . . . 4  |-  ( A  e.  CC  ->  (
( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  0 )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
137132, 136sylan9eqr 2527 . . 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 2515 . 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 808 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 189    \/ wo 375    /\ wa 376    \/_ wxo 1430    = wceq 1452  haddwhad 1504  caddwcad 1517    e. wcel 1904   ifcif 3872  (class class class)co 6308   CCcc 9555   0cc0 9557    + caddc 9560    x. cmul 9562   2c2 10681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-xor 1431  df-tru 1455  df-had 1505  df-cad 1518  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-po 4760  df-so 4761  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 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-pnf 9695  df-mnf 9696  df-ltxr 9698  df-2 10690
This theorem is referenced by:  sadadd2lem  14512
  Copyright terms: Public domain W3C validator