This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )