resmgmhm

Description: Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		resmgmhm.u	$⊢ U = S ↾_{𝑠} X$
2		mgmhmrcl	$⊢ F \in (S MgmHom T) \to (S \in Mgm \land T \in Mgm)$
3	2	simprd	$⊢ F \in (S MgmHom T) \to T \in Mgm$
4	1	submgmmgm	$⊢ X \in SubMgm (S) \to U \in Mgm$
5	3 4	anim12ci	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to (U \in Mgm \land T \in Mgm)$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7		eqid	$⊢ {Base}_{T} = {Base}_{T}$
8	6 7	mgmhmf	$⊢ F \in (S MgmHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
9	6	submgmss	$⊢ X \in SubMgm (S) \to X \subseteq {Base}_{S}$
10		fssres	$⊢ (F : {Base}_{S} ⟶ {Base}_{T} \land X \subseteq {Base}_{S}) \to ({F ↾}_{X}) : X ⟶ {Base}_{T}$
11	8 9 10	syl2an	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to ({F ↾}_{X}) : X ⟶ {Base}_{T}$
12	9	adantl	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to X \subseteq {Base}_{S}$
13	1 6	ressbas2	$⊢ X \subseteq {Base}_{S} \to X = {Base}_{U}$
14	12 13	syl	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to X = {Base}_{U}$
15	14	feq2d	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to (({F ↾}_{X}) : X ⟶ {Base}_{T} \leftrightarrow ({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T})$
16	11 15	mpbid	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to ({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T}$
17		simpll	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to F \in (S MgmHom T)$
18	9	ad2antlr	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to X \subseteq {Base}_{S}$
19		simprl	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to x \in X$
20	18 19	sseldd	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to x \in {Base}_{S}$
21		simprr	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to y \in X$
22	18 21	sseldd	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to y \in {Base}_{S}$
23		eqid	$⊢ +_{S} = +_{S}$
24		eqid	$⊢ +_{T} = +_{T}$
25	6 23 24	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)$
26	17 20 22 25	syl3anc	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to F (x +_{S} y) = F (x) +_{T} F (y)$
27	23	submgmcl	$⊢ (X \in SubMgm (S) \land x \in X \land y \in X) \to x +_{S} y \in X$
28	27	3expb	$⊢ (X \in SubMgm (S) \land (x \in X \land y \in X)) \to x +_{S} y \in X$
29	28	adantll	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to x +_{S} y \in X$
30		fvres	$⊢ x +_{S} y \in X \to ({F ↾}_{X}) (x +_{S} y) = F (x +_{S} y)$
31	29 30	syl	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to ({F ↾}_{X}) (x +_{S} y) = F (x +_{S} y)$
32		fvres	$⊢ x \in X \to ({F ↾}_{X}) (x) = F (x)$
33		fvres	$⊢ y \in X \to ({F ↾}_{X}) (y) = F (y)$
34	32 33	oveqan12d	$⊢ (x \in X \land y \in X) \to ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) = F (x) +_{T} F (y)$
35	34	adantl	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) = F (x) +_{T} F (y)$
36	26 31 35	3eqtr4d	$⊢ ((F \in (S MgmHom T) \land X \in SubMgm (S)) \land (x \in X \land y \in X)) \to ({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)$
37	36	ralrimivva	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to \forall x \in X \forall y \in X ({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)$
38	1 23	ressplusg	$⊢ X \in SubMgm (S) \to +_{S} = +_{U}$
39	38	adantl	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to +_{S} = +_{U}$
40	39	oveqd	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to x +_{S} y = x +_{U} y$
41	40	fveqeq2d	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to (({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) \leftrightarrow ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y))$
42	14 41	raleqbidv	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to (\forall y \in X ({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) \leftrightarrow \forall y \in {Base}_{U} ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y))$
43	14 42	raleqbidv	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to (\forall x \in X \forall y \in X ({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) \leftrightarrow \forall x \in {Base}_{U} \forall y \in {Base}_{U} ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y))$
44	37 43	mpbid	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to \forall x \in {Base}_{U} \forall y \in {Base}_{U} ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)$
45	16 44	jca	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to (({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T} \land \forall x \in {Base}_{U} \forall y \in {Base}_{U} ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y))$
46		eqid	$⊢ {Base}_{U} = {Base}_{U}$
47		eqid	$⊢ +_{U} = +_{U}$
48	46 7 47 24	ismgmhm	$⊢ {F ↾}_{X} \in (U MgmHom T) \leftrightarrow ((U \in Mgm \land T \in Mgm) \land (({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T} \land \forall x \in {Base}_{U} \forall y \in {Base}_{U} ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)))$
49	5 45 48	sylanbrc	$⊢ (F \in (S MgmHom T) \land X \in SubMgm (S)) \to {F ↾}_{X} \in (U MgmHom T)$

Metamath Proof Explorer

Theorem resmgmhm

Proof