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 ⊢ 𝑈 = ( 𝑆 ↾s 𝑋 )
Assertion resghm ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ ( SubGrp ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 GrpHom 𝑇 ) )

Proof

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