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 ( 𝐴 ·P 𝐵 ) = ( 𝐵 ·P 𝐴 )

Proof

Step Hyp Ref Expression
1 mpv ( ( 𝐴P𝐵P ) → ( 𝐴 ·P 𝐵 ) = { 𝑥 ∣ ∃ 𝑧𝐴𝑦𝐵 𝑥 = ( 𝑧 ·Q 𝑦 ) } )
2 mpv ( ( 𝐵P𝐴P ) → ( 𝐵 ·P 𝐴 ) = { 𝑥 ∣ ∃ 𝑦𝐵𝑧𝐴 𝑥 = ( 𝑦 ·Q 𝑧 ) } )
3 mulcomnq ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
4 3 eqeq2i ( 𝑥 = ( 𝑦 ·Q 𝑧 ) ↔ 𝑥 = ( 𝑧 ·Q 𝑦 ) )
5 4 2rexbii ( ∃ 𝑦𝐵𝑧𝐴 𝑥 = ( 𝑦 ·Q 𝑧 ) ↔ ∃ 𝑦𝐵𝑧𝐴 𝑥 = ( 𝑧 ·Q 𝑦 ) )
6 rexcom ( ∃ 𝑦𝐵𝑧𝐴 𝑥 = ( 𝑧 ·Q 𝑦 ) ↔ ∃ 𝑧𝐴𝑦𝐵 𝑥 = ( 𝑧 ·Q 𝑦 ) )
7 5 6 bitri ( ∃ 𝑦𝐵𝑧𝐴 𝑥 = ( 𝑦 ·Q 𝑧 ) ↔ ∃ 𝑧𝐴𝑦𝐵 𝑥 = ( 𝑧 ·Q 𝑦 ) )
8 7 abbii { 𝑥 ∣ ∃ 𝑦𝐵𝑧𝐴 𝑥 = ( 𝑦 ·Q 𝑧 ) } = { 𝑥 ∣ ∃ 𝑧𝐴𝑦𝐵 𝑥 = ( 𝑧 ·Q 𝑦 ) }
9 2 8 eqtrdi ( ( 𝐵P𝐴P ) → ( 𝐵 ·P 𝐴 ) = { 𝑥 ∣ ∃ 𝑧𝐴𝑦𝐵 𝑥 = ( 𝑧 ·Q 𝑦 ) } )
10 9 ancoms ( ( 𝐴P𝐵P ) → ( 𝐵 ·P 𝐴 ) = { 𝑥 ∣ ∃ 𝑧𝐴𝑦𝐵 𝑥 = ( 𝑧 ·Q 𝑦 ) } )
11 1 10 eqtr4d ( ( 𝐴P𝐵P ) → ( 𝐴 ·P 𝐵 ) = ( 𝐵 ·P 𝐴 ) )
12 dmmp dom ·P = ( P × P )
13 12 ndmovcom ( ¬ ( 𝐴P𝐵P ) → ( 𝐴 ·P 𝐵 ) = ( 𝐵 ·P 𝐴 ) )
14 11 13 pm2.61i ( 𝐴 ·P 𝐵 ) = ( 𝐵 ·P 𝐴 )