Metamath Proof Explorer

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 ⊢ A ⋅ 𝑷 B ⋅ 𝑷 C = A ⋅ 𝑷 B ⋅ 𝑷 C

Proof

Step Hyp Ref Expression
1 df-mp ⊢ ⋅ 𝑷 = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y ⋅ 𝑸 z
2 mulclnq ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y ⋅ 𝑸 z ∈ 𝑸
3 dmmp ⊢ dom ⁡ ⋅ 𝑷 = 𝑷 × 𝑷
4 mulclpr ⊢ f ∈ 𝑷 ∧ g ∈ 𝑷 → f ⋅ 𝑷 g ∈ 𝑷
5 mulassnq ⊢ f ⋅ 𝑸 g ⋅ 𝑸 h = f ⋅ 𝑸 g ⋅ 𝑸 h
6 1 2 3 4 5 genpass ⊢ A ⋅ 𝑷 B ⋅ 𝑷 C = A ⋅ 𝑷 B ⋅ 𝑷 C