Metamath Proof Explorer

Theorem rhmima

Description: The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion rhmima ⊢ F ∈ M RingHom N ∧ X ∈ SubRing ⁡ M → F X ∈ SubRing ⁡ N

Proof

Step Hyp Ref Expression
1 rhmghm ⊢ F ∈ M RingHom N → F ∈ M GrpHom N
2 subrgsubg ⊢ X ∈ SubRing ⁡ M → X ∈ SubGrp ⁡ M
3 ghmima ⊢ F ∈ M GrpHom N ∧ X ∈ SubGrp ⁡ M → F X ∈ SubGrp ⁡ N
4 1 2 3 syl2an ⊢ F ∈ M RingHom N ∧ X ∈ SubRing ⁡ M → F X ∈ SubGrp ⁡ N
5 eqid ⊢ mulGrp M = mulGrp M
6 eqid ⊢ mulGrp N = mulGrp N
7 5 6 rhmmhm ⊢ F ∈ M RingHom N → F ∈ mulGrp M MndHom mulGrp N
8 5 subrgsubm ⊢ X ∈ SubRing ⁡ M → X ∈ SubMnd ⁡ mulGrp M
9 mhmima ⊢ F ∈ mulGrp M MndHom mulGrp N ∧ X ∈ SubMnd ⁡ mulGrp M → F X ∈ SubMnd ⁡ mulGrp N
10 7 8 9 syl2an ⊢ F ∈ M RingHom N ∧ X ∈ SubRing ⁡ M → F X ∈ SubMnd ⁡ mulGrp N
11 rhmrcl2 ⊢ F ∈ M RingHom N → N ∈ Ring
12 11 adantr ⊢ F ∈ M RingHom N ∧ X ∈ SubRing ⁡ M → N ∈ Ring
13 6 issubrg3 ⊢ N ∈ Ring → F X ∈ SubRing ⁡ N ↔ F X ∈ SubGrp ⁡ N ∧ F X ∈ SubMnd ⁡ mulGrp N
14 12 13 syl ⊢ F ∈ M RingHom N ∧ X ∈ SubRing ⁡ M → F X ∈ SubRing ⁡ N ↔ F X ∈ SubGrp ⁡ N ∧ F X ∈ SubMnd ⁡ mulGrp N
15 4 10 14 mpbir2and ⊢ F ∈ M RingHom N ∧ X ∈ SubRing ⁡ M → F X ∈ SubRing ⁡ N