Theorem addcomprg 7568

Description: Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)

Assertion

Ref	Expression
addcomprg	|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = ( B +P. A ) )

Proof of Theorem addcomprg

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prop 7465	. . . . . . . . 9 |- ( B e. P. -> <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. )
2		elprnql 7471	. . . . . . . . 9 |- ( ( <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. /\ y e. ( 1st ` B ) ) -> y e. Q. )
3	1, 2	sylan 283	. . . . . . . 8 |- ( ( B e. P. /\ y e. ( 1st ` B ) ) -> y e. Q. )
4		prop 7465	. . . . . . . . . . . . 13 |- ( A e. P. -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. )
5		elprnql 7471	. . . . . . . . . . . . 13 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ z e. ( 1st ` A ) ) -> z e. Q. )
6	4, 5	sylan 283	. . . . . . . . . . . 12 |- ( ( A e. P. /\ z e. ( 1st ` A ) ) -> z e. Q. )
7		addcomnqg 7371	. . . . . . . . . . . . 13 |- ( ( y e. Q. /\ z e. Q. ) -> ( y +Q z ) = ( z +Q y ) )
8	7	eqeq2d 2189	. . . . . . . . . . . 12 |- ( ( y e. Q. /\ z e. Q. ) -> ( x = ( y +Q z ) <-> x = ( z +Q y ) ) )
9	6, 8	sylan2 286	. . . . . . . . . . 11 |- ( ( y e. Q. /\ ( A e. P. /\ z e. ( 1st ` A ) ) ) -> ( x = ( y +Q z ) <-> x = ( z +Q y ) ) )
10	9	anassrs 400	. . . . . . . . . 10 |- ( ( ( y e. Q. /\ A e. P. ) /\ z e. ( 1st ` A ) ) -> ( x = ( y +Q z ) <-> x = ( z +Q y ) ) )
11	10	rexbidva 2474	. . . . . . . . 9 |- ( ( y e. Q. /\ A e. P. ) -> ( E. z e. ( 1st ` A ) x = ( y +Q z ) <-> E. z e. ( 1st ` A ) x = ( z +Q y ) ) )
12	11	ancoms 268	. . . . . . . 8 |- ( ( A e. P. /\ y e. Q. ) -> ( E. z e. ( 1st ` A ) x = ( y +Q z ) <-> E. z e. ( 1st ` A ) x = ( z +Q y ) ) )
13	3, 12	sylan2 286	. . . . . . 7 |- ( ( A e. P. /\ ( B e. P. /\ y e. ( 1st ` B ) ) ) -> ( E. z e. ( 1st ` A ) x = ( y +Q z ) <-> E. z e. ( 1st ` A ) x = ( z +Q y ) ) )
14	13	anassrs 400	. . . . . 6 |- ( ( ( A e. P. /\ B e. P. ) /\ y e. ( 1st ` B ) ) -> ( E. z e. ( 1st ` A ) x = ( y +Q z ) <-> E. z e. ( 1st ` A ) x = ( z +Q y ) ) )
15	14	rexbidva 2474	. . . . 5 |- ( ( A e. P. /\ B e. P. ) -> ( E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( y +Q z ) <-> E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( z +Q y ) ) )
16		rexcom 2641	. . . . 5 |- ( E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( z +Q y ) <-> E. z e. ( 1st ` A ) E. y e. ( 1st ` B ) x = ( z +Q y ) )
17	15, 16	bitrdi 196	. . . 4 |- ( ( A e. P. /\ B e. P. ) -> ( E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( y +Q z ) <-> E. z e. ( 1st ` A ) E. y e. ( 1st ` B ) x = ( z +Q y ) ) )
18	17	rabbidv 2726	. . 3 |- ( ( A e. P. /\ B e. P. ) -> { x e. Q. | E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( y +Q z ) } = { x e. Q. | E. z e. ( 1st ` A ) E. y e. ( 1st ` B ) x = ( z +Q y ) } )
19		elprnqu 7472	. . . . . . . . 9 |- ( ( <. ( 1st ` B ) , ( 2nd ` B ) >. e. P. /\ y e. ( 2nd ` B ) ) -> y e. Q. )
20	1, 19	sylan 283	. . . . . . . 8 |- ( ( B e. P. /\ y e. ( 2nd ` B ) ) -> y e. Q. )
21		elprnqu 7472	. . . . . . . . . . . . 13 |- ( ( <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. /\ z e. ( 2nd ` A ) ) -> z e. Q. )
22	4, 21	sylan 283	. . . . . . . . . . . 12 |- ( ( A e. P. /\ z e. ( 2nd ` A ) ) -> z e. Q. )
23	22, 8	sylan2 286	. . . . . . . . . . 11 |- ( ( y e. Q. /\ ( A e. P. /\ z e. ( 2nd ` A ) ) ) -> ( x = ( y +Q z ) <-> x = ( z +Q y ) ) )
24	23	anassrs 400	. . . . . . . . . 10 |- ( ( ( y e. Q. /\ A e. P. ) /\ z e. ( 2nd ` A ) ) -> ( x = ( y +Q z ) <-> x = ( z +Q y ) ) )
25	24	rexbidva 2474	. . . . . . . . 9 |- ( ( y e. Q. /\ A e. P. ) -> ( E. z e. ( 2nd ` A ) x = ( y +Q z ) <-> E. z e. ( 2nd ` A ) x = ( z +Q y ) ) )
26	25	ancoms 268	. . . . . . . 8 |- ( ( A e. P. /\ y e. Q. ) -> ( E. z e. ( 2nd ` A ) x = ( y +Q z ) <-> E. z e. ( 2nd ` A ) x = ( z +Q y ) ) )
27	20, 26	sylan2 286	. . . . . . 7 |- ( ( A e. P. /\ ( B e. P. /\ y e. ( 2nd ` B ) ) ) -> ( E. z e. ( 2nd ` A ) x = ( y +Q z ) <-> E. z e. ( 2nd ` A ) x = ( z +Q y ) ) )
28	27	anassrs 400	. . . . . 6 |- ( ( ( A e. P. /\ B e. P. ) /\ y e. ( 2nd ` B ) ) -> ( E. z e. ( 2nd ` A ) x = ( y +Q z ) <-> E. z e. ( 2nd ` A ) x = ( z +Q y ) ) )
29	28	rexbidva 2474	. . . . 5 |- ( ( A e. P. /\ B e. P. ) -> ( E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( y +Q z ) <-> E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( z +Q y ) ) )
30		rexcom 2641	. . . . 5 |- ( E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( z +Q y ) <-> E. z e. ( 2nd ` A ) E. y e. ( 2nd ` B ) x = ( z +Q y ) )
31	29, 30	bitrdi 196	. . . 4 |- ( ( A e. P. /\ B e. P. ) -> ( E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( y +Q z ) <-> E. z e. ( 2nd ` A ) E. y e. ( 2nd ` B ) x = ( z +Q y ) ) )
32	31	rabbidv 2726	. . 3 |- ( ( A e. P. /\ B e. P. ) -> { x e. Q. | E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( y +Q z ) } = { x e. Q. | E. z e. ( 2nd ` A ) E. y e. ( 2nd ` B ) x = ( z +Q y ) } )
33	18, 32	opeq12d 3784	. 2 |- ( ( A e. P. /\ B e. P. ) -> <. { x e. Q. | E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( y +Q z ) } , { x e. Q. | E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( y +Q z ) } >. = <. { x e. Q. | E. z e. ( 1st ` A ) E. y e. ( 1st ` B ) x = ( z +Q y ) } , { x e. Q. | E. z e. ( 2nd ` A ) E. y e. ( 2nd ` B ) x = ( z +Q y ) } >. )
34		plpvlu 7528	. . 3 |- ( ( B e. P. /\ A e. P. ) -> ( B +P. A ) = <. { x e. Q. | E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( y +Q z ) } , { x e. Q. | E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( y +Q z ) } >. )
35	34	ancoms 268	. 2 |- ( ( A e. P. /\ B e. P. ) -> ( B +P. A ) = <. { x e. Q. | E. y e. ( 1st ` B ) E. z e. ( 1st ` A ) x = ( y +Q z ) } , { x e. Q. | E. y e. ( 2nd ` B ) E. z e. ( 2nd ` A ) x = ( y +Q z ) } >. )
36		plpvlu 7528	. 2 |- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = <. { x e. Q. | E. z e. ( 1st ` A ) E. y e. ( 1st ` B ) x = ( z +Q y ) } , { x e. Q. | E. z e. ( 2nd ` A ) E. y e. ( 2nd ` B ) x = ( z +Q y ) } >. )
37	33, 35, 36	3eqtr4rd 2221	1 |- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = ( B +P. A ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   E.wrex 2456   {crab 2459   <.cop 3594   ` cfv 5212  (class class class)co 5869   1stc1st 6133   2ndc2nd 6134   Q.cnq 7270   +Q cplq 7272   P.cnp 7281   +P. cpp 7283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-oadd 6415  df-omul 6416  df-er 6529  df-ec 6531  df-qs 6535  df-ni 7294  df-pli 7295  df-mi 7296  df-plpq 7334  df-enq 7337  df-nqqs 7338  df-plqqs 7339  df-inp 7456  df-iplp 7458

This theorem is referenced by:  prplnqu  7610  addextpr  7611  caucvgprlemcanl  7634  caucvgprprlemnkltj  7679  caucvgprprlemnbj  7683  caucvgprprlemmu  7685  caucvgprprlemloc  7693  caucvgprprlemexbt  7696  caucvgprprlemexb  7697  caucvgprprlemaddq  7698  enrer  7725  addcmpblnr  7729  mulcmpblnrlemg  7730  ltsrprg  7737  addcomsrg  7745  mulcomsrg  7747  mulasssrg  7748  distrsrg  7749  lttrsr  7752  ltposr  7753  ltsosr  7754  0lt1sr  7755  0idsr  7757  1idsr  7758  ltasrg  7760  recexgt0sr  7763  mulgt0sr  7768  aptisr  7769  mulextsr1lem  7770  archsr  7772  srpospr  7773  prsrpos  7775  prsradd  7776  prsrlt  7777  ltpsrprg  7793  map2psrprg  7795  pitonnlem1p1  7836  pitoregt0  7839  recidpirqlemcalc  7847