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	$$⊢\left(A{\cdot }_{𝑷}B\right){\cdot }_{𝑷}C=A{\cdot }_{𝑷}\left(B{\cdot }_{𝑷}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-mp	$$⊢{\cdot }_{𝑷}=\left(w\in 𝑷,v\in 𝑷⟼\left\{x|\exists y\in w\exists z\in vx=y{\cdot }_{𝑸}z\right\}\right)$$
2		mulclnq	$$⊢\left(y\in 𝑸\wedge z\in 𝑸\right)\to y{\cdot }_{𝑸}z\in 𝑸$$
3		dmmp	$$⊢\mathrm{dom}{\cdot }_{𝑷}=𝑷\times 𝑷$$
4		mulclpr	$$⊢\left(f\in 𝑷\wedge g\in 𝑷\right)\to f{\cdot }_{𝑷}g\in 𝑷$$
5		mulassnq	$$⊢\left(f{\cdot }_{𝑸}g\right){\cdot }_{𝑸}h=f{\cdot }_{𝑸}\left(g{\cdot }_{𝑸}h\right)$$
6	1 2 3 4 5	genpass	$$⊢\left(A{\cdot }_{𝑷}B\right){\cdot }_{𝑷}C=A{\cdot }_{𝑷}\left(B{\cdot }_{𝑷}C\right)$$