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 \in (S GrpHom T) \land X \in SubGrp (S)) \to {F ↾}_{X} \in (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 \in SubGrp (S) \to U \in Grp$
7	6	adantl	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to U \in Grp$
8		ghmgrp2	$⊢ F \in (S GrpHom T) \to T \in Grp$
9	8	adantr	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to T \in Grp$
10		eqid	$⊢ {Base}_{S} = {Base}_{S}$
11	10 3	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
12	10	subgss	$⊢ X \in SubGrp (S) \to X \subseteq {Base}_{S}$
13		fssres	$⊢ (F : {Base}_{S} ⟶ {Base}_{T} \land X \subseteq {Base}_{S}) \to ({F ↾}_{X}) : X ⟶ {Base}_{T}$
14	11 12 13	syl2an	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to ({F ↾}_{X}) : X ⟶ {Base}_{T}$
15	12	adantl	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to X \subseteq {Base}_{S}$
16	1 10	ressbas2	$⊢ X \subseteq {Base}_{S} \to X = {Base}_{U}$
17	15 16	syl	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to X = {Base}_{U}$
18	17	feq2d	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to (({F ↾}_{X}) : X ⟶ {Base}_{T} \leftrightarrow ({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T})$
19	14 18	mpbid	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to ({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T}$
20		eleq2	$⊢ X = {Base}_{U} \to (a \in X \leftrightarrow a \in {Base}_{U})$
21		eleq2	$⊢ X = {Base}_{U} \to (b \in X \leftrightarrow b \in {Base}_{U})$
22	20 21	anbi12d	$⊢ X = {Base}_{U} \to ((a \in X \land b \in X) \leftrightarrow (a \in {Base}_{U} \land b \in {Base}_{U}))$
23	17 22	syl	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to ((a \in X \land b \in X) \leftrightarrow (a \in {Base}_{U} \land b \in {Base}_{U}))$
24	23	biimpar	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in {Base}_{U} \land b \in {Base}_{U})) \to (a \in X \land b \in X)$
25		simpll	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to F \in (S GrpHom T)$
26	15	sselda	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land a \in X) \to a \in {Base}_{S}$
27	26	adantrr	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to a \in {Base}_{S}$
28	15	sselda	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land b \in X) \to b \in {Base}_{S}$
29	28	adantrl	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to b \in {Base}_{S}$
30		eqid	$⊢ +_{S} = +_{S}$
31	10 30 5	ghmlin	$⊢ (F \in (S GrpHom T) \land a \in {Base}_{S} \land b \in {Base}_{S}) \to F (a +_{S} b) = F (a) +_{T} F (b)$
32	25 27 29 31	syl3anc	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to F (a +_{S} b) = F (a) +_{T} F (b)$
33	1 30	ressplusg	$⊢ X \in SubGrp (S) \to +_{S} = +_{U}$
34	33	ad2antlr	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to +_{S} = +_{U}$
35	34	oveqd	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to a +_{S} b = a +_{U} b$
36	35	fveq2d	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to ({F ↾}_{X}) (a +_{S} b) = ({F ↾}_{X}) (a +_{U} b)$
37	30	subgcl	$⊢ (X \in SubGrp (S) \land a \in X \land b \in X) \to a +_{S} b \in X$
38	37	3expb	$⊢ (X \in SubGrp (S) \land (a \in X \land b \in X)) \to a +_{S} b \in X$
39	38	adantll	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to a +_{S} b \in X$
40	39	fvresd	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to ({F ↾}_{X}) (a +_{S} b) = F (a +_{S} b)$
41	36 40	eqtr3d	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to ({F ↾}_{X}) (a +_{U} b) = F (a +_{S} b)$
42		fvres	$⊢ a \in X \to ({F ↾}_{X}) (a) = F (a)$
43		fvres	$⊢ b \in X \to ({F ↾}_{X}) (b) = F (b)$
44	42 43	oveqan12d	$⊢ (a \in X \land b \in X) \to ({F ↾}_{X}) (a) +_{T} ({F ↾}_{X}) (b) = F (a) +_{T} F (b)$
45	44	adantl	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to ({F ↾}_{X}) (a) +_{T} ({F ↾}_{X}) (b) = F (a) +_{T} F (b)$
46	32 41 45	3eqtr4d	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in X \land b \in X)) \to ({F ↾}_{X}) (a +_{U} b) = ({F ↾}_{X}) (a) +_{T} ({F ↾}_{X}) (b)$
47	24 46	syldan	$⊢ ((F \in (S GrpHom T) \land X \in SubGrp (S)) \land (a \in {Base}_{U} \land b \in {Base}_{U})) \to ({F ↾}_{X}) (a +_{U} b) = ({F ↾}_{X}) (a) +_{T} ({F ↾}_{X}) (b)$
48	2 3 4 5 7 9 19 47	isghmd	$⊢ (F \in (S GrpHom T) \land X \in SubGrp (S)) \to {F ↾}_{X} \in (U GrpHom T)$

Metamath Proof Explorer

Theorem resghm

Proof