resmgmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		resmgmhm2.u	$⊢ U = T ↾_{𝑠} X$
2		mgmhmrcl	$⊢ F \in (S MgmHom T) \to (S \in Mgm \land T \in Mgm)$
3	2	simpld	$⊢ F \in (S MgmHom T) \to S \in Mgm$
4	3	adantl	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to S \in Mgm$
5	1	submgmmgm	$⊢ X \in SubMgm (T) \to U \in Mgm$
6	5	ad2antrr	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to U \in Mgm$
7	4 6	jca	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to (S \in Mgm \land U \in Mgm)$
8		eqid	$⊢ {Base}_{S} = {Base}_{S}$
9		eqid	$⊢ {Base}_{T} = {Base}_{T}$
10	8 9	mgmhmf	$⊢ F \in (S MgmHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
11	10	adantl	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to F : {Base}_{S} ⟶ {Base}_{T}$
12	11	ffnd	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to F Fn {Base}_{S}$
13		simplr	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to ran F \subseteq X$
14		df-f	$⊢ F : {Base}_{S} ⟶ X \leftrightarrow (F Fn {Base}_{S} \land ran F \subseteq X)$
15	12 13 14	sylanbrc	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to F : {Base}_{S} ⟶ X$
16	1	submgmbas	$⊢ X \in SubMgm (T) \to X = {Base}_{U}$
17	16	ad2antrr	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to X = {Base}_{U}$
18	17	feq3d	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to (F : {Base}_{S} ⟶ X \leftrightarrow F : {Base}_{S} ⟶ {Base}_{U})$
19	15 18	mpbid	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to F : {Base}_{S} ⟶ {Base}_{U}$
20		eqid	$⊢ +_{S} = +_{S}$
21		eqid	$⊢ +_{T} = +_{T}$
22	8 20 21	mgmhmlin	$⊢ (F \in (S MgmHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to F (x +_{S} y) = F (x) +_{T} F (y)$
23	22	3expb	$⊢ (F \in (S MgmHom T) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{T} F (y)$
24	23	adantll	$⊢ (((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{T} F (y)$
25	1 21	ressplusg	$⊢ X \in SubMgm (T) \to +_{T} = +_{U}$
26	25	ad3antrrr	$⊢ (((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to +_{T} = +_{U}$
27	26	oveqd	$⊢ (((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x) +_{T} F (y) = F (x) +_{U} F (y)$
28	24 27	eqtrd	$⊢ (((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (x +_{S} y) = F (x) +_{U} F (y)$
29	28	ralrimivva	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to \forall x \in {Base}_{S} \forall y \in {Base}_{S} F (x +_{S} y) = F (x) +_{U} F (y)$
30	19 29	jca	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom 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))$
31		eqid	$⊢ {Base}_{U} = {Base}_{U}$
32		eqid	$⊢ +_{U} = +_{U}$
33	8 31 20 32	ismgmhm	$⊢ F \in (S MgmHom U) \leftrightarrow ((S \in Mgm \land U \in Mgm) \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)))$
34	7 30 33	sylanbrc	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom T)) \to F \in (S MgmHom U)$
35	1	resmgmhm2	$⊢ (F \in (S MgmHom U) \land X \in SubMgm (T)) \to F \in (S MgmHom T)$
36	35	ancoms	$⊢ (X \in SubMgm (T) \land F \in (S MgmHom U)) \to F \in (S MgmHom T)$
37	36	adantlr	$⊢ ((X \in SubMgm (T) \land ran F \subseteq X) \land F \in (S MgmHom U)) \to F \in (S MgmHom T)$
38	34 37	impbida	$⊢ (X \in SubMgm (T) \land ran F \subseteq X) \to (F \in (S MgmHom T) \leftrightarrow F \in (S MgmHom U))$

Metamath Proof Explorer

Theorem resmgmhm2b

Proof