resmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		resmhm2.u	$⊢ U = T ↾_{𝑠} X$
2		mhmrcl1	$⊢ F \in (S MndHom T) \to S \in Mnd$
3	2	adantl	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to S \in Mnd$
4	1	submmnd	$⊢ X \in SubMnd (T) \to U \in Mnd$
5	4	ad2antrr	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to U \in Mnd$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7		eqid	$⊢ {Base}_{T} = {Base}_{T}$
8	6 7	mhmf	$⊢ F \in (S MndHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
9	8	adantl	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
10	9	ffnd	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F Fn {Base}_{S}$
11		simplr	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to ran F \subseteq X$
12		df-f	$⊢ F : {Base}_{S} ⟶ X \leftrightarrow (F Fn {Base}_{S} \land ran F \subseteq X)$
13	10 11 12	sylanbrc	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F : {Base}_{S} ⟶ X$
14	1	submbas	$⊢ X \in SubMnd (T) \to X = {Base}_{U}$
15	14	ad2antrr	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to X = {Base}_{U}$
16	15	feq3d	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to (F : {Base}_{S} ⟶ X \leftrightarrow F : {Base}_{S} ⟶ {Base}_{U})$
17	13 16	mpbid	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F : {Base}_{S} ⟶ {Base}_{U}$
18		eqid	$⊢ +_{S} = +_{S}$
19		eqid	$⊢ +_{T} = +_{T}$
20	6 18 19	mhmlin	$⊢ (F \in (S MndHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{T} F (y)$
21	20	3expb	$⊢ (F \in (S MndHom T) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{T} F (y)$
22	21	adantll	$⊢ (((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{T} F (y)$
23	1 19	ressplusg	$⊢ X \in SubMnd (T) \to +_{T} = +_{U}$
24	23	ad3antrrr	$⊢ (((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to +_{T} = +_{U}$
25	24	oveqd	$⊢ (((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x) +_{T} F (y) = F (x) +_{U} F (y)$
26	22 25	eqtrd	$⊢ (((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{U} F (y)$
27	26	ralrimivva	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{U} F (y)$
28		eqid	$⊢ 0_{S} = 0_{S}$
29		eqid	$⊢ 0_{T} = 0_{T}$
30	28 29	mhm0	$⊢ F \in (S MndHom T) \to F (0_{S}) = 0_{T}$
31	30	adantl	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F (0_{S}) = 0_{T}$
32	1 29	subm0	$⊢ X \in SubMnd (T) \to 0_{T} = 0_{U}$
33	32	ad2antrr	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to 0_{T} = 0_{U}$
34	31 33	eqtrd	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F (0_{S}) = 0_{U}$
35	17 27 34	3jca	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to (F : {Base}_{S} ⟶ {Base}_{U} \land \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{U} F (y) \land F (0_{S}) = 0_{U})$
36		eqid	$⊢ {Base}_{U} = {Base}_{U}$
37		eqid	$⊢ +_{U} = +_{U}$
38		eqid	$⊢ 0_{U} = 0_{U}$
39	6 36 18 37 28 38	ismhm	$⊢ F \in (S MndHom U) \leftrightarrow ((S \in Mnd \land U \in Mnd) \land (F : {Base}_{S} ⟶ {Base}_{U} \land \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{U} F (y) \land F (0_{S}) = 0_{U}))$
40	3 5 35 39	syl21anbrc	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom T)) \to F \in (S MndHom U)$
41	1	resmhm2	$⊢ (F \in (S MndHom U) \land X \in SubMnd (T)) \to F \in (S MndHom T)$
42	41	ancoms	$⊢ (X \in SubMnd (T) \land F \in (S MndHom U)) \to F \in (S MndHom T)$
43	42	adantlr	$⊢ ((X \in SubMnd (T) \land ran F \subseteq X) \land F \in (S MndHom U)) \to F \in (S MndHom T)$
44	40 43	impbida	$⊢ (X \in SubMnd (T) \land ran F \subseteq X) \to (F \in (S MndHom T) \leftrightarrow F \in (S MndHom U))$

Metamath Proof Explorer

Theorem resmhm2b

Proof