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 )