Theorem addcompr

Description: Addition of positive reals is commutative. Proposition 9-3.5(ii) of Gleason p. 123. (Contributed by NM, 19-Nov-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addcompr	|- ( A +P. B ) = ( B +P. A )

Proof

Step	Hyp	Ref	Expression
1		plpv	|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = { x | E. z e. A E. y e. B x = ( z +Q y ) } )
2		plpv	|- ( ( B e. P. /\ A e. P. ) -> ( B +P. A ) = { x | E. y e. B E. z e. A x = ( y +Q z ) } )
3		addcomnq	|- ( y +Q z ) = ( z +Q y )
4	3	eqeq2i	|- ( x = ( y +Q z ) <-> x = ( z +Q y ) )
5	4	2rexbii	|- ( E. y e. B E. z e. A x = ( y +Q z ) <-> E. y e. B E. z e. A x = ( z +Q y ) )
6		rexcom	|- ( E. y e. B E. z e. A x = ( z +Q y ) <-> E. z e. A E. y e. B x = ( z +Q y ) )
7	5 6	bitri	|- ( E. y e. B E. z e. A x = ( y +Q z ) <-> E. z e. A E. y e. B x = ( z +Q y ) )
8	7	abbii	|- { x | E. y e. B E. z e. A x = ( y +Q z ) } = { x | E. z e. A E. y e. B x = ( z +Q y ) }
9	2 8	eqtrdi	|- ( ( B e. P. /\ A e. P. ) -> ( B +P. A ) = { x | E. z e. A E. y e. B x = ( z +Q y ) } )
10	9	ancoms	|- ( ( A e. P. /\ B e. P. ) -> ( B +P. A ) = { x | E. z e. A E. y e. B x = ( z +Q y ) } )
11	1 10	eqtr4d	|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = ( B +P. A ) )
12		dmplp	|- dom +P. = ( P. X. P. )
13	12	ndmovcom	|- ( -. ( A e. P. /\ B e. P. ) -> ( A +P. B ) = ( B +P. A ) )
14	11 13	pm2.61i	|- ( A +P. B ) = ( B +P. A )