Theorem axmulrcl

Description: Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl be used later. Instead, in most cases use remulcl . (New usage is discouraged.) (Contributed by NM, 31-Mar-1996)

	Ref	Expression
Assertion	axmulrcl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		elreal	|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
2		elreal	|- ( B e. RR <-> E. y e. R. <. y , 0R >. = B )
3		oveq1	|- ( <. x , 0R >. = A -> ( <. x , 0R >. x. <. y , 0R >. ) = ( A x. <. y , 0R >. ) )
4	3	eleq1d	|- ( <. x , 0R >. = A -> ( ( <. x , 0R >. x. <. y , 0R >. ) e. RR <-> ( A x. <. y , 0R >. ) e. RR ) )
5		oveq2	|- ( <. y , 0R >. = B -> ( A x. <. y , 0R >. ) = ( A x. B ) )
6	5	eleq1d	|- ( <. y , 0R >. = B -> ( ( A x. <. y , 0R >. ) e. RR <-> ( A x. B ) e. RR ) )
7		mulresr	|- ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. x. <. y , 0R >. ) = <. ( x .R y ) , 0R >. )
8		mulclsr	|- ( ( x e. R. /\ y e. R. ) -> ( x .R y ) e. R. )
9		opelreal	|- ( <. ( x .R y ) , 0R >. e. RR <-> ( x .R y ) e. R. )
10	8 9	sylibr	|- ( ( x e. R. /\ y e. R. ) -> <. ( x .R y ) , 0R >. e. RR )
11	7 10	eqeltrd	|- ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. x. <. y , 0R >. ) e. RR )
12	1 2 4 6 11	2gencl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )