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 𝐴 )