Theorem mulcompr

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

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

Proof

Step	Hyp	Ref	Expression
1		mpv	|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) = { x | E. z e. A E. y e. B x = ( z .Q y ) } )
2		mpv	|- ( ( B e. P. /\ A e. P. ) -> ( B .P. A ) = { x | E. y e. B E. z e. A x = ( y .Q z ) } )
3		mulcomnq	|- ( 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		dmmp	|- 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 )