Theorem rnrhmsubrg

Description: The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023)

	Ref	Expression
Assertion	rnrhmsubrg	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ran 𝐹 ∈ ( SubRing ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ima	⊢ ( 𝐹 “ ( Base ‘ 𝑀 ) ) = ran ( 𝐹 ↾ ( Base ‘ 𝑀 ) )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3		eqid	⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
4	2 3	rhmf	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
5	4	ffnd	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
6		fnresdm	⊢ ( 𝐹 Fn ( Base ‘ 𝑀 ) → ( 𝐹 ↾ ( Base ‘ 𝑀 ) ) = 𝐹 )
7	5 6	syl	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( 𝐹 ↾ ( Base ‘ 𝑀 ) ) = 𝐹 )
8	7	rneqd	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ran ( 𝐹 ↾ ( Base ‘ 𝑀 ) ) = ran 𝐹 )
9	1 8	eqtr2id	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ran 𝐹 = ( 𝐹 “ ( Base ‘ 𝑀 ) ) )
10		rhmrcl1	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝑀 ∈ Ring )
11	2	subrgid	⊢ ( 𝑀 ∈ Ring → ( Base ‘ 𝑀 ) ∈ ( SubRing ‘ 𝑀 ) )
12	10 11	syl	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( Base ‘ 𝑀 ) ∈ ( SubRing ‘ 𝑀 ) )
13		rhmima	⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ ( Base ‘ 𝑀 ) ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ ( Base ‘ 𝑀 ) ) ∈ ( SubRing ‘ 𝑁 ) )
14	12 13	mpdan	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( 𝐹 “ ( Base ‘ 𝑀 ) ) ∈ ( SubRing ‘ 𝑁 ) )
15	9 14	eqeltrd	⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ran 𝐹 ∈ ( SubRing ‘ 𝑁 ) )