Metamath Proof Explorer

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 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
2 eqid ⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 )
3 1 2 rhmf ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) )
4 3 ffnd ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 Fn ( Base ‘ 𝑀 ) )
5 fnima ⊢ ( 𝐹 Fn ( Base ‘ 𝑀 ) → ( 𝐹 “ ( Base ‘ 𝑀 ) ) = ran 𝐹 )
6 4 5 syl ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( 𝐹 “ ( Base ‘ 𝑀 ) ) = ran 𝐹 )
7 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝑀 ∈ Ring )
8 1 subrgid ⊢ ( 𝑀 ∈ Ring → ( Base ‘ 𝑀 ) ∈ ( SubRing ‘ 𝑀 ) )
9 7 8 syl ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( Base ‘ 𝑀 ) ∈ ( SubRing ‘ 𝑀 ) )
10 rhmima ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ ( Base ‘ 𝑀 ) ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ ( Base ‘ 𝑀 ) ) ∈ ( SubRing ‘ 𝑁 ) )
11 9 10 mpdan ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ( 𝐹 “ ( Base ‘ 𝑀 ) ) ∈ ( SubRing ‘ 𝑁 ) )
12 6 11 eqeltrrd ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → ran 𝐹 ∈ ( SubRing ‘ 𝑁 ) )