Metamath Proof Explorer

Theorem rngohomcl

Description: Obsolete theorem, use rhmcl instead. Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rnghomf.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	rnghomf.2	⊢ 𝑋 = ran 𝐺
	rnghomf.3	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
	rnghomf.4	⊢ 𝑌 = ran 𝐽
Assertion	rngohomcl	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		rnghomf.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		rnghomf.2	⊢ 𝑋 = ran 𝐺
3		rnghomf.3	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
4		rnghomf.4	⊢ 𝑌 = ran 𝐽
5	1 2 3 4	rngohomf	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
6	5	ffvelcdmda	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑌 )