Theorem rngohomcl

Description: Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011)

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

Proof

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