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 .P. B ) .P. C ) = ( A .P. ( B .P. C ) )

Proof

Step	Hyp	Ref	Expression
1		df-mp	|- .P. = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y .Q z ) } )
2		mulclnq	|- ( ( y e. Q. /\ z e. Q. ) -> ( y .Q z ) e. Q. )
3		dmmp	|- dom .P. = ( P. X. P. )
4		mulclpr	|- ( ( f e. P. /\ g e. P. ) -> ( f .P. g ) e. P. )
5		mulassnq	|- ( ( f .Q g ) .Q h ) = ( f .Q ( g .Q h ) )
6	1 2 3 4 5	genpass	|- ( ( A .P. B ) .P. C ) = ( A .P. ( B .P. C ) )