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	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	ringi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	ringi.3	⊢ 𝑋 = ran 𝐺
Assertion	rngocl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ringi.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		ringi.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		ringi.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	rngosm	⊢ ( 𝑅 ∈ RingOps → 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
5		fovrn	⊢ ( ( 𝐻 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
6	4 5	syl3an1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )