Theorem mulclpr

Description: Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of Gleason p. 124. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	mulclpr	|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) e. P. )

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		ltmnq	|- ( h e. Q. -> ( f ( h .Q f )
4		mulcomnq	|- ( x .Q y ) = ( y .Q x )
5		mulclprlem	|- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x x e. ( A .P. B ) ) )
6	1 2 3 4 5	genpcl	|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) e. P. )