Theorem mulasspr

Description: Multiplication of positive reals is associative. Proposition 9-3.7(i) of Gleason p. 124. (Contributed by NM, 18-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	mulasspr	⊢ ( ( 𝐴 ·P 𝐵 ) ·P 𝐶 ) = ( 𝐴 ·P ( 𝐵 ·P 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-mp	⊢ ·P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 ·Q 𝑧 ) } )
2		mulclnq	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 ·Q 𝑧 ) ∈ Q )
3		dmmp	⊢ dom ·P = ( P × P )
4		mulclpr	⊢ ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ) → ( 𝑓 ·P 𝑔 ) ∈ P )
5		mulassnq	⊢ ( ( 𝑓 ·Q 𝑔 ) ·Q ℎ ) = ( 𝑓 ·Q ( 𝑔 ·Q ℎ ) )
6	1 2 3 4 5	genpass	⊢ ( ( 𝐴 ·P 𝐵 ) ·P 𝐶 ) = ( 𝐴 ·P ( 𝐵 ·P 𝐶 ) )