resmhm2

Description: One direction of resmhm2b . (Contributed by Mario Carneiro, 18-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		resmhm2.u	$⊢ U = T ↾_{𝑠} X$
2		mhmrcl1	$⊢ F \in (S MndHom U) \to S \in Mnd$
3		submrcl	$⊢ X \in SubMnd (T) \to T \in Mnd$
4	2 3	anim12i	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to (S \in Mnd \land T \in Mnd)$
5		eqid	$⊢ {Base}_{S} = {Base}_{S}$
6		eqid	$⊢ {Base}_{U} = {Base}_{U}$
7	5 6	mhmf	$⊢ F \in (S MndHom U) \to F : {Base}_{S} ⟶ {Base}_{U}$
8	1	submbas	$⊢ X \in SubMnd (T) \to X = {Base}_{U}$
9		eqid	$⊢ {Base}_{T} = {Base}_{T}$
10	9	submss	$⊢ X \in SubMnd (T) \to X \subseteq {Base}_{T}$
11	8 10	eqsstrrd	$⊢ X \in SubMnd (T) \to {Base}_{U} \subseteq {Base}_{T}$
12		fss	$⊢ (F : {Base}_{S} ⟶ {Base}_{U} \land {Base}_{U} \subseteq {Base}_{T}) \to F : {Base}_{S} ⟶ {Base}_{T}$
13	7 11 12	syl2an	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
14		eqid	$⊢ +_{S} = +_{S}$
15		eqid	$⊢ +_{U} = +_{U}$
16	5 14 15	mhmlin	$⊢ (F \in (S MndHom U) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{U} F (y)$
17	16	3expb	$⊢ (F \in (S MndHom U) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{U} F (y)$
18	17	adantlr	$⊢ ((F \in (S MndHom U) \land X \in SubMnd (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{U} F (y)$
19		eqid	$⊢ +_{T} = +_{T}$
20	1 19	ressplusg	$⊢ X \in SubMnd (T) \to +_{T} = +_{U}$
21	20	ad2antlr	$⊢ ((F \in (S MndHom U) \land X \in SubMnd (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to +_{T} = +_{U}$
22	21	oveqd	$⊢ ((F \in (S MndHom U) \land X \in SubMnd (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x) +_{T} F (y) = F (x) +_{U} F (y)$
23	18 22	eqtr4d	$⊢ ((F \in (S MndHom U) \land X \in SubMnd (T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{T} F (y)$
24	23	ralrimivva	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{T} F (y)$
25		eqid	$⊢ 0_{S} = 0_{S}$
26		eqid	$⊢ 0_{U} = 0_{U}$
27	25 26	mhm0	$⊢ F \in (S MndHom U) \to F (0_{S}) = 0_{U}$
28	27	adantr	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to F (0_{S}) = 0_{U}$
29		eqid	$⊢ 0_{T} = 0_{T}$
30	1 29	subm0	$⊢ X \in SubMnd (T) \to 0_{T} = 0_{U}$
31	30	adantl	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to 0_{T} = 0_{U}$
32	28 31	eqtr4d	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to F (0_{S}) = 0_{T}$
33	13 24 32	3jca	$⊢ (F \in (S MndHom U) \land X \in SubMnd (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) \land F (0_{S}) = 0_{T})$
34	5 9 14 19 25 29	ismhm	$⊢ F \in (S MndHom T) \leftrightarrow ((S \in Mnd \land T \in Mnd) \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) \land F (0_{S}) = 0_{T}))$
35	4 33 34	sylanbrc	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to F \in (S MndHom T)$

Metamath Proof Explorer

Theorem resmhm2

Proof