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 e. ( M RingHom N ) /\ X e. ( SubRing ` M ) ) -> ( F " X ) e. ( SubRing ` N ) )

Proof

Step Hyp Ref Expression
1 rhmghm 
 |-  ( F e. ( M RingHom N ) -> F e. ( M GrpHom N ) )
2 subrgsubg 
 |-  ( X e. ( SubRing ` M ) -> X e. ( SubGrp ` M ) )
3 ghmima 
 |-  ( ( F e. ( M GrpHom N ) /\ X e. ( SubGrp ` M ) ) -> ( F " X ) e. ( SubGrp ` N ) )
4 1 2 3 syl2an 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRing ` M ) ) -> ( F " X ) e. ( SubGrp ` N ) )
5 eqid 
 |-  ( mulGrp ` M ) = ( mulGrp ` M )
6 eqid 
 |-  ( mulGrp ` N ) = ( mulGrp ` N )
7 5 6 rhmmhm 
 |-  ( F e. ( M RingHom N ) -> F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) )
8 5 subrgsubm 
 |-  ( X e. ( SubRing ` M ) -> X e. ( SubMnd ` ( mulGrp ` M ) ) )
9 mhmima 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubMnd ` ( mulGrp ` M ) ) ) -> ( F " X ) e. ( SubMnd ` ( mulGrp ` N ) ) )
10 7 8 9 syl2an 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRing ` M ) ) -> ( F " X ) e. ( SubMnd ` ( mulGrp ` N ) ) )
11 rhmrcl2 
 |-  ( F e. ( M RingHom N ) -> N e. Ring )
12 11 adantr 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRing ` M ) ) -> N e. Ring )
13 6 issubrg3 
 |-  ( N e. Ring -> ( ( F " X ) e. ( SubRing ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ ( F " X ) e. ( SubMnd ` ( mulGrp ` N ) ) ) ) )
14 12 13 syl 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRing ` M ) ) -> ( ( F " X ) e. ( SubRing ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ ( F " X ) e. ( SubMnd ` ( mulGrp ` N ) ) ) ) )
15 4 10 14 mpbir2and 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRing ` M ) ) -> ( F " X ) e. ( SubRing ` N ) )