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 ⊢ F ∈ M RingHom N → ran ⁡ F ∈ SubRing ⁡ N

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base M = Base M
2 eqid ⊢ Base N = Base N
3 1 2 rhmf ⊢ F ∈ M RingHom N → F : Base M ⟶ Base N
4 3 ffnd ⊢ F ∈ M RingHom N → F Fn Base M
5 fnima ⊢ F Fn Base M → F Base M = ran ⁡ F
6 4 5 syl ⊢ F ∈ M RingHom N → F Base M = ran ⁡ F
7 rhmrcl1 ⊢ F ∈ M RingHom N → M ∈ Ring
8 1 subrgid ⊢ M ∈ Ring → Base M ∈ SubRing ⁡ M
9 7 8 syl ⊢ F ∈ M RingHom N → Base M ∈ SubRing ⁡ M
10 rhmima ⊢ F ∈ M RingHom N ∧ Base M ∈ SubRing ⁡ M → F Base M ∈ SubRing ⁡ N
11 9 10 mpdan ⊢ F ∈ M RingHom N → F Base M ∈ SubRing ⁡ N
12 6 11 eqeltrrd ⊢ F ∈ M RingHom N → ran ⁡ F ∈ SubRing ⁡ N