This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 rhmghm ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) )
2 subrgsubg ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑀 ) → 𝑋 ∈ ( SubGrp ‘ 𝑀 ) )
3 ghmima ⊢ ( ( 𝐹 ∈ ( 𝑀 GrpHom 𝑁 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) )
5 eqid ⊢ ( mulGrp ‘ 𝑀 ) = ( mulGrp ‘ 𝑀 )
6 eqid ⊢ ( mulGrp ‘ 𝑁 ) = ( mulGrp ‘ 𝑁 )
7 5 6 rhmmhm ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) )
8 5 subrgsubm ⊢ ( 𝑋 ∈ ( SubRing ‘ 𝑀 ) → 𝑋 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑀 ) ) )
9 mhmima ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑀 ) MndHom ( mulGrp ‘ 𝑁 ) ) ∧ 𝑋 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑀 ) ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) )
10 7 8 9 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) )
11 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) → 𝑁 ∈ Ring )
12 11 adantr ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → 𝑁 ∈ Ring )
13 6 issubrg3 ⊢ ( 𝑁 ∈ Ring → ( ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) ∧ ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) ) ) )
14 12 13 syl ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) ↔ ( ( 𝐹 “ 𝑋 ) ∈ ( SubGrp ‘ 𝑁 ) ∧ ( 𝐹 “ 𝑋 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑁 ) ) ) ) )
15 4 10 14 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑀 RingHom 𝑁 ) ∧ 𝑋 ∈ ( SubRing ‘ 𝑀 ) ) → ( 𝐹 “ 𝑋 ) ∈ ( SubRing ‘ 𝑁 ) )