Theorem rngocl

Description: Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringi.1	|- G = ( 1st ` R )
	ringi.2	|- H = ( 2nd ` R )
	ringi.3	|- X = ran G
Assertion	rngocl	|- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	|- G = ( 1st ` R )
2		ringi.2	|- H = ( 2nd ` R )
3		ringi.3	|- X = ran G
4	1 2 3	rngosm	|- ( R e. RingOps -> H : ( X X. X ) --> X )
5		fovcdm	|- ( ( H : ( X X. X ) --> X /\ A e. X /\ B e. X ) -> ( A H B ) e. X )
6	4 5	syl3an1	|- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )