resmgmhm2

		Ref	Expression
	Hypothesis	resmgmhm2.u	$⊢ U = T ↾_{𝑠} X$
	Assertion	resmgmhm2	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to F \in (S MgmHom T)$

Proof

Step	Hyp	Ref	Expression
1		resmgmhm2.u	$⊢ U = T ↾_{𝑠} X$
2		mgmhmrcl	$⊢ F \in (S MgmHom U) \to (S \in Mgm \land U \in Mgm)$
3	2	simpld	$⊢ F \in (S MgmHom U) \to S \in Mgm$
4		submgmrcl	$⊢ X \in SubMgm (T) \to T \in Mgm$
5	3 4	anim12i	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to (S \in Mgm \land T \in Mgm)$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7		eqid	$⊢ {Base}_{U} = {Base}_{U}$
8	6 7	mgmhmf	$⊢ F \in (S MgmHom U) \to F : {Base}_{S} ⟶ {Base}_{U}$
9	1	submgmbas	$⊢ X \in SubMgm (T) \to X = {Base}_{U}$
10		eqid	$⊢ {Base}_{T} = {Base}_{T}$
11	10	submgmss	$⊢ X \in SubMgm (T) \to X \subseteq {Base}_{T}$
12	9 11	eqsstrrd	$⊢ X \in SubMgm (T) \to {Base}_{U} \subseteq {Base}_{T}$
13		fss	$⊢ (F : {Base}_{S} ⟶ {Base}_{U} \land {Base}_{U} \subseteq {Base}_{T}) \to F : {Base}_{S} ⟶ {Base}_{T}$
14	8 12 13	syl2an	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
15		eqid	$⊢ +_{S} = +_{S}$
16		eqid	$⊢ +_{U} = +_{U}$
17	6 15 16	mgmhmlin	$⊢ (F \in (S MgmHom U) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{U} F (y)$
18	17	3expb	$⊢ (F \in (S MgmHom U) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{U} F (y)$
19	18	adantlr	$⊢ ((F \in (S MgmHom U) \land X \in SubMgm (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{U} F (y)$
20		eqid	$⊢ +_{T} = +_{T}$
21	1 20	ressplusg	$⊢ X \in SubMgm (T) \to +_{T} = +_{U}$
22	21	ad2antlr	$⊢ ((F \in (S MgmHom U) \land X \in SubMgm (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to +_{T} = +_{U}$
23	22	oveqd	$⊢ ((F \in (S MgmHom U) \land X \in SubMgm (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x) +_{T} F (y) = F (x) +_{U} F (y)$
24	19 23	eqtr4d	$⊢ ((F \in (S MgmHom U) \land X \in SubMgm (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{T} F (y)$
25	24	ralrimivva	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{T} F (y)$
26	14 25	jca	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to (F : {Base}_{S} ⟶ {Base}_{T} \land \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{T} F (y))$
27	6 10 15 20	ismgmhm	$⊢ F \in (S MgmHom T) \leftrightarrow ((S \in Mgm \land T \in Mgm) \land (F : {Base}_{S} ⟶ {Base}_{T} \land \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{T} F (y)))$
28	5 26 27	sylanbrc	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to F \in (S MgmHom T)$

Metamath Proof Explorer

Theorem resmgmhm2

Proof