Metamath Proof Explorer

Theorem resrhm

Description: Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Hypothesis resrhm.u 
|- U = ( S |`s X )
Assertion resrhm 
|- ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( F |` X ) e. ( U RingHom T ) )

Proof

Step Hyp Ref Expression
1 resrhm.u 
 |-  U = ( S |`s X )
2 rhmrcl2 
 |-  ( F e. ( S RingHom T ) -> T e. Ring )
3 1 subrgring 
 |-  ( X e. ( SubRing ` S ) -> U e. Ring )
4 2 3 anim12ci 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( U e. Ring /\ T e. Ring ) )
5 rhmghm 
 |-  ( F e. ( S RingHom T ) -> F e. ( S GrpHom T ) )
6 subrgsubg 
 |-  ( X e. ( SubRing ` S ) -> X e. ( SubGrp ` S ) )
7 1 resghm 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( F |` X ) e. ( U GrpHom T ) )
8 5 6 7 syl2an 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( F |` X ) e. ( U GrpHom T ) )
9 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
10 eqid 
 |-  ( mulGrp ` T ) = ( mulGrp ` T )
11 9 10 rhmmhm 
 |-  ( F e. ( S RingHom T ) -> F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) )
12 9 subrgsubm 
 |-  ( X e. ( SubRing ` S ) -> X e. ( SubMnd ` ( mulGrp ` S ) ) )
13 eqid 
 |-  ( ( mulGrp ` S ) |`s X ) = ( ( mulGrp ` S ) |`s X )
14 13 resmhm 
 |-  ( ( F e. ( ( mulGrp ` S ) MndHom ( mulGrp ` T ) ) /\ X e. ( SubMnd ` ( mulGrp ` S ) ) ) -> ( F |` X ) e. ( ( ( mulGrp ` S ) |`s X ) MndHom ( mulGrp ` T ) ) )
15 11 12 14 syl2an 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( F |` X ) e. ( ( ( mulGrp ` S ) |`s X ) MndHom ( mulGrp ` T ) ) )
16 rhmrcl1 
 |-  ( F e. ( S RingHom T ) -> S e. Ring )
17 1 9 mgpress 
 |-  ( ( S e. Ring /\ X e. ( SubRing ` S ) ) -> ( ( mulGrp ` S ) |`s X ) = ( mulGrp ` U ) )
18 16 17 sylan 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( ( mulGrp ` S ) |`s X ) = ( mulGrp ` U ) )
19 18 oveq1d 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( ( ( mulGrp ` S ) |`s X ) MndHom ( mulGrp ` T ) ) = ( ( mulGrp ` U ) MndHom ( mulGrp ` T ) ) )
20 15 19 eleqtrd 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( F |` X ) e. ( ( mulGrp ` U ) MndHom ( mulGrp ` T ) ) )
21 8 20 jca 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( ( F |` X ) e. ( U GrpHom T ) /\ ( F |` X ) e. ( ( mulGrp ` U ) MndHom ( mulGrp ` T ) ) ) )
22 eqid 
 |-  ( mulGrp ` U ) = ( mulGrp ` U )
23 22 10 isrhm 
 |-  ( ( F |` X ) e. ( U RingHom T ) <-> ( ( U e. Ring /\ T e. Ring ) /\ ( ( F |` X ) e. ( U GrpHom T ) /\ ( F |` X ) e. ( ( mulGrp ` U ) MndHom ( mulGrp ` T ) ) ) ) )
24 4 21 23 sylanbrc 
 |-  ( ( F e. ( S RingHom T ) /\ X e. ( SubRing ` S ) ) -> ( F |` X ) e. ( U RingHom T ) )