Metamath Proof Explorer

Theorem rhmimasubrng

Description: The homomorphic image of a subring is a subring. (Contributed by AV, 16-Feb-2025)

Ref Expression
Assertion rhmimasubrng 
|- ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubRng ` N ) )

Proof

Step Hyp Ref Expression
1 rhmghm 
 |-  ( F e. ( M RingHom N ) -> F e. ( M GrpHom N ) )
2 subrngsubg 
 |-  ( X e. ( SubRng ` 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. ( SubRng ` 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 simpl 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) )
9 eqid 
 |-  ( Base ` M ) = ( Base ` M )
10 5 9 mgpbas 
 |-  ( Base ` M ) = ( Base ` ( mulGrp ` M ) )
11 10 eqcomi 
 |-  ( Base ` ( mulGrp ` M ) ) = ( Base ` M )
12 11 subrngss 
 |-  ( X e. ( SubRng ` M ) -> X C_ ( Base ` ( mulGrp ` M ) ) )
13 12 adantl 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> X C_ ( Base ` ( mulGrp ` M ) ) )
14 eqidd 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> ( +g ` ( mulGrp ` M ) ) = ( +g ` ( mulGrp ` M ) ) )
15 eqidd 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> ( +g ` ( mulGrp ` N ) ) = ( +g ` ( mulGrp ` N ) ) )
16 eqid 
 |-  ( .r ` M ) = ( .r ` M )
17 5 16 mgpplusg 
 |-  ( .r ` M ) = ( +g ` ( mulGrp ` M ) )
18 17 eqcomi 
 |-  ( +g ` ( mulGrp ` M ) ) = ( .r ` M )
19 18 subrngmcl 
 |-  ( ( X e. ( SubRng ` M ) /\ z e. X /\ x e. X ) -> ( z ( +g ` ( mulGrp ` M ) ) x ) e. X )
20 19 3adant1l 
 |-  ( ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) /\ z e. X /\ x e. X ) -> ( z ( +g ` ( mulGrp ` M ) ) x ) e. X )
21 8 13 14 15 20 mhmimalem 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` ( mulGrp ` N ) ) y ) e. ( F " X ) )
22 eqid 
 |-  ( .r ` N ) = ( .r ` N )
23 6 22 mgpplusg 
 |-  ( .r ` N ) = ( +g ` ( mulGrp ` N ) )
24 23 eqcomi 
 |-  ( +g ` ( mulGrp ` N ) ) = ( .r ` N )
25 24 oveqi 
 |-  ( x ( +g ` ( mulGrp ` N ) ) y ) = ( x ( .r ` N ) y )
26 25 eleq1i 
 |-  ( ( x ( +g ` ( mulGrp ` N ) ) y ) e. ( F " X ) <-> ( x ( .r ` N ) y ) e. ( F " X ) )
27 26 2ralbii 
 |-  ( A. x e. ( F " X ) A. y e. ( F " X ) ( x ( +g ` ( mulGrp ` N ) ) y ) e. ( F " X ) <-> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) )
28 21 27 sylib 
 |-  ( ( F e. ( ( mulGrp ` M ) MndHom ( mulGrp ` N ) ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) )
29 7 28 sylan 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) )
30 rhmrcl2 
 |-  ( F e. ( M RingHom N ) -> N e. Ring )
31 ringrng 
 |-  ( N e. Ring -> N e. Rng )
32 30 31 syl 
 |-  ( F e. ( M RingHom N ) -> N e. Rng )
33 32 adantr 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> N e. Rng )
34 eqid 
 |-  ( Base ` N ) = ( Base ` N )
35 34 22 issubrng2 
 |-  ( N e. Rng -> ( ( F " X ) e. ( SubRng ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) ) )
36 33 35 syl 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( ( F " X ) e. ( SubRng ` N ) <-> ( ( F " X ) e. ( SubGrp ` N ) /\ A. x e. ( F " X ) A. y e. ( F " X ) ( x ( .r ` N ) y ) e. ( F " X ) ) ) )
37 4 29 36 mpbir2and 
 |-  ( ( F e. ( M RingHom N ) /\ X e. ( SubRng ` M ) ) -> ( F " X ) e. ( SubRng ` N ) )