Metamath Proof Explorer

Theorem resghm

Description: Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypothesis resghm.u 
|- U = ( S |`s X )
Assertion resghm 
|- ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( F |` X ) e. ( U GrpHom T ) )

Proof

Step Hyp Ref Expression
1 resghm.u 
 |-  U = ( S |`s X )
2 eqid 
 |-  ( Base ` U ) = ( Base ` U )
3 eqid 
 |-  ( Base ` T ) = ( Base ` T )
4 eqid 
 |-  ( +g ` U ) = ( +g ` U )
5 eqid 
 |-  ( +g ` T ) = ( +g ` T )
6 1 subggrp 
 |-  ( X e. ( SubGrp ` S ) -> U e. Grp )
7 6 adantl 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> U e. Grp )
8 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
9 8 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> T e. Grp )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 10 3 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
12 10 subgss 
 |-  ( X e. ( SubGrp ` S ) -> X C_ ( Base ` S ) )
13 fssres 
 |-  ( ( F : ( Base ` S ) --> ( Base ` T ) /\ X C_ ( Base ` S ) ) -> ( F |` X ) : X --> ( Base ` T ) )
14 11 12 13 syl2an 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( F |` X ) : X --> ( Base ` T ) )
15 12 adantl 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> X C_ ( Base ` S ) )
16 1 10 ressbas2 
 |-  ( X C_ ( Base ` S ) -> X = ( Base ` U ) )
17 15 16 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> X = ( Base ` U ) )
18 17 feq2d 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( ( F |` X ) : X --> ( Base ` T ) <-> ( F |` X ) : ( Base ` U ) --> ( Base ` T ) ) )
19 14 18 mpbid 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( F |` X ) : ( Base ` U ) --> ( Base ` T ) )
20 eleq2 
 |-  ( X = ( Base ` U ) -> ( a e. X <-> a e. ( Base ` U ) ) )
21 eleq2 
 |-  ( X = ( Base ` U ) -> ( b e. X <-> b e. ( Base ` U ) ) )
22 20 21 anbi12d 
 |-  ( X = ( Base ` U ) -> ( ( a e. X /\ b e. X ) <-> ( a e. ( Base ` U ) /\ b e. ( Base ` U ) ) ) )
23 17 22 syl 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( ( a e. X /\ b e. X ) <-> ( a e. ( Base ` U ) /\ b e. ( Base ` U ) ) ) )
24 23 biimpar 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. ( Base ` U ) /\ b e. ( Base ` U ) ) ) -> ( a e. X /\ b e. X ) )
25 simpll 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> F e. ( S GrpHom T ) )
26 15 sselda 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ a e. X ) -> a e. ( Base ` S ) )
27 26 adantrr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> a e. ( Base ` S ) )
28 15 sselda 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ b e. X ) -> b e. ( Base ` S ) )
29 28 adantrl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> b e. ( Base ` S ) )
30 eqid 
 |-  ( +g ` S ) = ( +g ` S )
31 10 30 5 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ a e. ( Base ` S ) /\ b e. ( Base ` S ) ) -> ( F ` ( a ( +g ` S ) b ) ) = ( ( F ` a ) ( +g ` T ) ( F ` b ) ) )
32 25 27 29 31 syl3anc 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( F ` ( a ( +g ` S ) b ) ) = ( ( F ` a ) ( +g ` T ) ( F ` b ) ) )
33 1 30 ressplusg 
 |-  ( X e. ( SubGrp ` S ) -> ( +g ` S ) = ( +g ` U ) )
34 33 ad2antlr 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( +g ` S ) = ( +g ` U ) )
35 34 oveqd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( a ( +g ` S ) b ) = ( a ( +g ` U ) b ) )
36 35 fveq2d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( ( F |` X ) ` ( a ( +g ` S ) b ) ) = ( ( F |` X ) ` ( a ( +g ` U ) b ) ) )
37 30 subgcl 
 |-  ( ( X e. ( SubGrp ` S ) /\ a e. X /\ b e. X ) -> ( a ( +g ` S ) b ) e. X )
38 37 3expb 
 |-  ( ( X e. ( SubGrp ` S ) /\ ( a e. X /\ b e. X ) ) -> ( a ( +g ` S ) b ) e. X )
39 38 adantll 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( a ( +g ` S ) b ) e. X )
40 39 fvresd 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( ( F |` X ) ` ( a ( +g ` S ) b ) ) = ( F ` ( a ( +g ` S ) b ) ) )
41 36 40 eqtr3d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( ( F |` X ) ` ( a ( +g ` U ) b ) ) = ( F ` ( a ( +g ` S ) b ) ) )
42 fvres 
 |-  ( a e. X -> ( ( F |` X ) ` a ) = ( F ` a ) )
43 fvres 
 |-  ( b e. X -> ( ( F |` X ) ` b ) = ( F ` b ) )
44 42 43 oveqan12d 
 |-  ( ( a e. X /\ b e. X ) -> ( ( ( F |` X ) ` a ) ( +g ` T ) ( ( F |` X ) ` b ) ) = ( ( F ` a ) ( +g ` T ) ( F ` b ) ) )
45 44 adantl 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( ( ( F |` X ) ` a ) ( +g ` T ) ( ( F |` X ) ` b ) ) = ( ( F ` a ) ( +g ` T ) ( F ` b ) ) )
46 32 41 45 3eqtr4d 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. X /\ b e. X ) ) -> ( ( F |` X ) ` ( a ( +g ` U ) b ) ) = ( ( ( F |` X ) ` a ) ( +g ` T ) ( ( F |` X ) ` b ) ) )
47 24 46 syldan 
 |-  ( ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) /\ ( a e. ( Base ` U ) /\ b e. ( Base ` U ) ) ) -> ( ( F |` X ) ` ( a ( +g ` U ) b ) ) = ( ( ( F |` X ) ` a ) ( +g ` T ) ( ( F |` X ) ` b ) ) )
48 2 3 4 5 7 9 19 47 isghmd 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. ( SubGrp ` S ) ) -> ( F |` X ) e. ( U GrpHom T ) )