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 ↾ 𝑠 X
Assertion resghm ⊢ F ∈ S GrpHom T ∧ X ∈ SubGrp ⁡ S → F ↾ X ∈ U GrpHom T

Proof

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