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

Theorem sadadd2lem2 12657
Description: The core of the proof of sadadd2 12667. 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 8847 . . . . . . . . 9  |-  0  e.  CC
2 ifcl 3614 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ps ,  A ,  0 )  e.  CC )
31, 2mpan2 652 . . . . . . . 8  |-  ( A  e.  CC  ->  if ( ps ,  A , 
0 )  e.  CC )
43ad2antrr 706 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ps ,  A ,  0 )  e.  CC )
5 simpll 730 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  A  e.  CC )
64, 5, 5add12d 9049 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
75, 4, 5addassd 8873 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
)  =  ( A  +  ( if ( ps ,  A , 
0 )  +  A
) ) )
86, 7eqtr4d 2331 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if ( ps ,  A , 
0 )  +  ( A  +  A ) )  =  ( ( A  +  if ( ps ,  A , 
0 ) )  +  A ) )
9 pm5.501 330 . . . . . . . . 9  |-  ( ph  ->  ( ps  <->  ( ph  <->  ps ) ) )
109adantl 452 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
1110bicomd 192 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( ph  <->  ps )  <->  ps ) )
1211ifbid 3596 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph 
<->  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
13 simpr 447 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ph )
1413orcd 381 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ph  \/  ps ) )
15 iftrue 3584 . . . . . . . 8  |-  ( (
ph  \/  ps )  ->  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A
) )
1614, 15syl 15 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
1752timesd 9970 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( 2  x.  A )  =  ( A  +  A ) )
1816, 17eqtrd 2328 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( (
ph  \/  ps ) ,  ( 2  x.  A ) ,  0 )  =  ( A  +  A ) )
1912, 18oveq12d 5892 . . . . 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 3584 . . . . . . . 8  |-  ( ph  ->  if ( ph ,  A ,  0 )  =  A )
2120adantl 452 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
2221oveq1d 5889 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
2322oveq1d 5889 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( ( A  +  if ( ps ,  A ,  0 ) )  +  A
) )
248, 19, 233eqtr4d 2338 . . . 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 3585 . . . . . . . . 9  |-  ( -. 
ph  ->  if ( ph ,  A ,  0 )  =  0 )
2625adantl 452 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
2726oveq1d 5889 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
283ad2antrr 706 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
2928addid2d 9029 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( 0  +  if ( ps ,  A ,  0 ) )  =  if ( ps ,  A ,  0 ) )
3027, 29eqtrd 2328 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  if ( ps ,  A ,  0 ) )
3130oveq1d 5889 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  A )  =  ( if ( ps ,  A , 
0 )  +  A
) )
32 2cn 9832 . . . . . . . . . . . . 13  |-  2  e.  CC
3332a1i 10 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  2  e.  CC )
34 id 19 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  A  e.  CC )
3533, 34mulcld 8871 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  (
2  x.  A )  e.  CC )
3635addid2d 9029 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( 2  x.  A ) )
37 2times 9859 . . . . . . . . . 10  |-  ( A  e.  CC  ->  (
2  x.  A )  =  ( A  +  A ) )
3836, 37eqtrd 2328 . . . . . . . . 9  |-  ( A  e.  CC  ->  (
0  +  ( 2  x.  A ) )  =  ( A  +  A ) )
3938adantr 451 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( 0  +  ( 2  x.  A ) )  =  ( A  +  A
) )
40 iftrue 3584 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
0 ,  A )  =  0 )
4140adantl 452 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  0 ,  A )  =  0 )
42 iftrue 3584 . . . . . . . . . 10  |-  ( ps 
->  if ( ps , 
( 2  x.  A
) ,  0 )  =  ( 2  x.  A ) )
4342adantl 452 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  ( 2  x.  A ) )
4441, 43oveq12d 5892 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( 0  +  ( 2  x.  A ) ) )
45 iftrue 3584 . . . . . . . . . 10  |-  ( ps 
->  if ( ps ,  A ,  0 )  =  A )
4645adantl 452 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ps )  ->  if ( ps ,  A , 
0 )  =  A )
4746oveq1d 5889 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( A  +  A ) )
4839, 44, 473eqtr4d 2338 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
49 simpl 443 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  A  e.  CC )
501a1i 10 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  0  e.  CC )
5149, 50addcomd 9030 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( A  +  0 )  =  ( 0  +  A ) )
52 iffalse 3585 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  0 ,  A
)  =  A )
5352adantl 452 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  0 ,  A )  =  A )
54 iffalse 3585 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5554adantl 452 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  0 )
5653, 55oveq12d 5892 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  0 ) )
57 iffalse 3585 . . . . . . . . . 10  |-  ( -. 
ps  ->  if ( ps ,  A ,  0 )  =  0 )
5857adantl 452 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  A , 
0 )  =  0 )
5958oveq1d 5889 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  A ,  0 )  +  A )  =  ( 0  +  A ) )
6051, 56, 593eqtr4d 2338 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6148, 60pm2.61dan 766 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
6261ad2antrr 706 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  A ) )
63 ifnot 3616 . . . . . . 7  |-  if ( -.  ps ,  A ,  0 )  =  if ( ps , 
0 ,  A )
64 nbn2 334 . . . . . . . . 9  |-  ( -. 
ph  ->  ( -.  ps  <->  (
ph 
<->  ps ) ) )
6564adantl 452 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
6665ifbid 3596 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( -.  ps ,  A , 
0 )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
6763, 66syl5eqr 2342 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  0 ,  A )  =  if ( ( ph  <->  ps ) ,  A ,  0 ) )
68 biorf 394 . . . . . . . 8  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
6968adantl 452 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  ( ps  <->  (
ph  \/  ps )
) )
7069ifbid 3596 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
ch )  /\  -.  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
7167, 70oveq12d 5892 . . . . 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 2335 . . . 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 766 . . 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 1380 . . . . . . 7  |-  (hadd ( ch ,  ph ,  ps )  <-> hadd ( ph ,  ps ,  ch ) )
75 had1 1392 . . . . . . 7  |-  ( ch 
->  (hadd ( ch ,  ph ,  ps )  <->  (
ph 
<->  ps ) ) )
7674, 75syl5bbr 250 . . . . . 6  |-  ( ch 
->  (hadd ( ph ,  ps ,  ch )  <->  (
ph 
<->  ps ) ) )
7776adantl 452 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (hadd (
ph ,  ps ,  ch )  <->  ( ph  <->  ps )
) )
7877ifbid 3596 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  <->  ps ) ,  A , 
0 ) )
79 cad1 1388 . . . . . 6  |-  ( ch 
->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  \/  ps )
) )
8079adantl 452 . . . . 5  |-  ( ( A  e.  CC  /\  ch )  ->  (cadd (
ph ,  ps ,  ch )  <->  ( ph  \/  ps ) ) )
8180ifbid 3596 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  \/  ps ) ,  ( 2  x.  A ) ,  0 ) )
8278, 81oveq12d 5892 . . 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 3584 . . . . 5  |-  ( ch 
->  if ( ch ,  A ,  0 )  =  A )
8483adantl 452 . . . 4  |-  ( ( A  e.  CC  /\  ch )  ->  if ( ch ,  A , 
0 )  =  A )
8584oveq2d 5890 . . 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 2338 . 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 ) ) )
8746oveq2d 5890 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ps )  ->  ( A  +  if ( ps ,  A ,  0 ) )  =  ( A  +  A ) )
8839, 44, 873eqtr4d 2338 . . . . . . 7  |-  ( ( A  e.  CC  /\  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
8955, 58eqtr4d 2331 . . . . . . . 8  |-  ( ( A  e.  CC  /\  -.  ps )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ps ,  A ,  0 ) )
9053, 89oveq12d 5892 . . . . . . 7  |-  ( ( A  e.  CC  /\  -.  ps )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9188, 90pm2.61dan 766 . . . . . 6  |-  ( A  e.  CC  ->  ( if ( ps ,  0 ,  A )  +  if ( ps , 
( 2  x.  A
) ,  0 ) )  =  ( A  +  if ( ps ,  A ,  0 ) ) )
9291ad2antrr 706 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if ( ps ,  0 ,  A )  +  if ( ps ,  ( 2  x.  A ) ,  0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
939adantl 452 . . . . . . . . . . 11  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  <->  ps ) ) )
9493notbid 285 . . . . . . . . . 10  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  -.  ( ph  <->  ps )
) )
95 df-xor 1296 . . . . . . . . . 10  |-  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
9694, 95syl6bbr 254 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( -.  ps  <->  (
ph  \/_  ps )
) )
9796ifbid 3596 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( -. 
ps ,  A , 
0 )  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
9863, 97syl5eqr 2342 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  0 ,  A
)  =  if ( ( ph  \/_  ps ) ,  A , 
0 ) )
99 ibar 490 . . . . . . . . 9  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
10099adantl 452 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
101100ifbid 3596 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ps ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )
10298, 101oveq12d 5892 . . . . . 6  |-  ( ( ( 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 ) ) )
103102eqcomd 2301 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if ( ( ph  \/_  ps ) ,  A , 
0 )  +  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  0 ,  A
)  +  if ( ps ,  ( 2  x.  A ) ,  0 ) ) )
10420adantl 452 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  if ( ph ,  A ,  0 )  =  A )
105104oveq1d 5889 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  ph )  ->  ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( A  +  if ( ps ,  A , 
0 ) ) )
10692, 103, 1053eqtr4d 2338 . . . 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 ) ) )
107 simplll 734 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  ps )  ->  A  e.  CC )
1081a1i 10 . . . . . . 7  |-  ( ( ( ( A  e.  CC  /\  -.  ch )  /\  -.  ph )  /\  -.  ps )  -> 
0  e.  CC )
109107, 108ifclda 3605 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ps ,  A , 
0 )  e.  CC )
1101a1i 10 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  0  e.  CC )
111109, 110addcomd 9030 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ps ,  A , 
0 )  +  0 )  =  ( 0  +  if ( ps ,  A ,  0 ) ) )
11264adantl 452 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ps 
<->  ( ph  <->  ps )
) )
113112con1bid 320 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( -.  ( ph  <->  ps )  <->  ps )
)
11495, 113syl5bb 248 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( ( ph  \/_  ps )  <->  ps )
)
115114ifbid 3596 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  \/_  ps ) ,  A ,  0 )  =  if ( ps ,  A ,  0 ) )
116 simpr 447 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ph )
117 simpl 443 . . . . . . . 8  |-  ( (
ph  /\  ps )  ->  ph )
118116, 117nsyl 113 . . . . . . 7  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  -.  ( ph  /\  ps ) )
119 iffalse 3585 . . . . . . 7  |-  ( -.  ( ph  /\  ps )  ->  if ( (
ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
120118, 119syl 15 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if (
( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 )  =  0 )
121115, 120oveq12d 5892 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ( ph  \/_  ps ) ,  A , 
0 )  +  if ( ( ph  /\  ps ) ,  ( 2  x.  A ) ,  0 ) )  =  ( if ( ps ,  A ,  0 )  +  0 ) )
12225adantl 452 . . . . . 6  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  if ( ph ,  A , 
0 )  =  0 )
123122oveq1d 5889 . . . . 5  |-  ( ( ( A  e.  CC  /\ 
-.  ch )  /\  -.  ph )  ->  ( if ( ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  =  ( 0  +  if ( ps ,  A , 
0 ) ) )
124111, 121, 1233eqtr4d 2338 . . . 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 ) ) )
125106, 124pm2.61dan 766 . . 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 ) ) )
126 had0 1393 . . . . . . 7  |-  ( -. 
ch  ->  (hadd ( ch ,  ph ,  ps ) 
<->  ( ph  \/_  ps ) ) )
12774, 126syl5bbr 250 . . . . . 6  |-  ( -. 
ch  ->  (hadd ( ph ,  ps ,  ch )  <->  (
ph  \/_  ps )
) )
128127adantl 452 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (hadd ( ph ,  ps ,  ch )  <->  ( ph  \/_  ps ) ) )
129128ifbid 3596 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (hadd ( ph ,  ps ,  ch ) ,  A ,  0 )  =  if ( ( ph  \/_ 
ps ) ,  A ,  0 ) )
130 cad0 1390 . . . . . 6  |-  ( -. 
ch  ->  (cadd ( ph ,  ps ,  ch )  <->  (
ph  /\  ps )
) )
131130adantl 452 . . . . 5  |-  ( ( A  e.  CC  /\  -.  ch )  ->  (cadd ( ph ,  ps ,  ch )  <->  ( ph  /\  ps ) ) )
132131ifbid 3596 . . . 4  |-  ( ( A  e.  CC  /\  -.  ch )  ->  if (cadd ( ph ,  ps ,  ch ) ,  ( 2  x.  A ) ,  0 )  =  if ( ( ph  /\ 
ps ) ,  ( 2  x.  A ) ,  0 ) )
133129, 132oveq12d 5892 . . 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 ) ) )
134 iffalse 3585 . . . . 5  |-  ( -. 
ch  ->  if ( ch ,  A ,  0 )  =  0 )
135134oveq2d 5890 . . . 4  |-  ( -. 
ch  ->  ( ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  if ( ch ,  A , 
0 ) )  =  ( ( if (
ph ,  A , 
0 )  +  if ( ps ,  A , 
0 ) )  +  0 ) )
136 ifcl 3614 . . . . . . 7  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  if ( ph ,  A ,  0 )  e.  CC )
1371, 136mpan2 652 . . . . . 6  |-  ( A  e.  CC  ->  if ( ph ,  A , 
0 )  e.  CC )
138137, 3addcld 8870 . . . . 5  |-  ( A  e.  CC  ->  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  e.  CC )
139138addid1d 9028 . . . 4  |-  ( A  e.  CC  ->  (
( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) )  +  0 )  =  ( if ( ph ,  A ,  0 )  +  if ( ps ,  A ,  0 ) ) )
140135, 139sylan9eqr 2350 . . 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 ) ) )
141125, 133, 1403eqtr4d 2338 . 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 ) ) )
14286, 141pm2.61dan 766 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 176    \/ wo 357    /\ wa 358    \/_ wxo 1295  haddwhad 1368  caddwcad 1369    = wceq 1632    e. wcel 1696   ifcif 3578  (class class class)co 5874   CCcc 8751   0cc0 8753    + caddc 8756    x. cmul 8758   2c2 9811
This theorem is referenced by:  sadadd2lem  12666
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-xor 1296  df-tru 1310  df-had 1370  df-cad 1371  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-po 4330  df-so 4331  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-pnf 8885  df-mnf 8886  df-ltxr 8888  df-2 9820
  Copyright terms: Public domain W3C validator