resmhm

Description: Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		resmhm.u	$⊢ U = S ↾_{𝑠} X$
2		mhmrcl2	$⊢ F \in (S MndHom T) \to T \in Mnd$
3	1	submmnd	$⊢ X \in SubMnd (S) \to U \in Mnd$
4	2 3	anim12ci	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to (U \in Mnd \land T \in Mnd)$
5		eqid	$⊢ {Base}_{S} = {Base}_{S}$
6		eqid	$⊢ {Base}_{T} = {Base}_{T}$
7	5 6	mhmf	$⊢ F \in (S MndHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
8	5	submss	$⊢ X \in SubMnd (S) \to X \subseteq {Base}_{S}$
9		fssres	$⊢ (F : {Base}_{S} ⟶ {Base}_{T} \land X \subseteq {Base}_{S}) \to ({F ↾}_{X}) : X ⟶ {Base}_{T}$
10	7 8 9	syl2an	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to ({F ↾}_{X}) : X ⟶ {Base}_{T}$
11	8	adantl	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to X \subseteq {Base}_{S}$
12	1 5	ressbas2	$⊢ X \subseteq {Base}_{S} \to X = {Base}_{U}$
13	11 12	syl	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to X = {Base}_{U}$
14	13	feq2d	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to (({F ↾}_{X}) : X ⟶ {Base}_{T} \leftrightarrow ({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T})$
15	10 14	mpbid	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to ({F ↾}_{X}) : {Base}_{U} ⟶ {Base}_{T}$
16		simpll	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to F \in (S MndHom T)$
17	8	ad2antlr	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to X \subseteq {Base}_{S}$
18		simprl	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to x \in X$
19	17 18	sseldd	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to x \in {Base}_{S}$
20		simprr	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to y \in X$
21	17 20	sseldd	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to y \in {Base}_{S}$
22		eqid	$⊢ +_{S} = +_{S}$
23		eqid	$⊢ +_{T} = +_{T}$
24	5 22 23	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)$
25	16 19 21 24	syl3anc	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to F (x +_{S} y) = F (x) +_{T} F (y)$
26	22	submcl	$⊢ (X \in SubMnd (S) \land x \in X \land y \in X) \to x +_{S} y \in X$
27	26	3expb	$⊢ (X \in SubMnd (S) \land (x \in X \land y \in X)) \to x +_{S} y \in X$
28	27	adantll	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to x +_{S} y \in X$
29	28	fvresd	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to ({F ↾}_{X}) (x +_{S} y) = F (x +_{S} y)$
30		fvres	$⊢ x \in X \to ({F ↾}_{X}) (x) = F (x)$
31		fvres	$⊢ y \in X \to ({F ↾}_{X}) (y) = F (y)$
32	30 31	oveqan12d	$⊢ (x \in X \land y \in X) \to ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) = F (x) +_{T} F (y)$
33	32	adantl	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y) = F (x) +_{T} F (y)$
34	25 29 33	3eqtr4d	$⊢ ((F \in (S MndHom T) \land X \in SubMnd (S)) \land (x \in X \land y \in X)) \to ({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)$
35	34	ralrimivva	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to \forall x \in X \forall y \in X ({F ↾}_{X}) (x +_{S} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)$
36	1 22	ressplusg	$⊢ X \in SubMnd (S) \to +_{S} = +_{U}$
37	36	adantl	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to +_{S} = +_{U}$
38	37	oveqd	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to x +_{S} y = x +_{U} y$
39	38	fveqeq2d	$⊢ (F \in (S MndHom T) \land X \in SubMnd (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))$
40	13 39	raleqbidv	$⊢ (F \in (S MndHom T) \land X \in SubMnd (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))$
41	13 40	raleqbidv	$⊢ (F \in (S MndHom T) \land X \in SubMnd (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))$
42	35 41	mpbid	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to \forall x \in {Base}_{U} \forall y \in {Base}_{U} ({F ↾}_{X}) (x +_{U} y) = ({F ↾}_{X}) (x) +_{T} ({F ↾}_{X}) (y)$
43		eqid	$⊢ 0_{S} = 0_{S}$
44	43	subm0cl	$⊢ X \in SubMnd (S) \to 0_{S} \in X$
45	44	adantl	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to 0_{S} \in X$
46	45	fvresd	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to ({F ↾}_{X}) (0_{S}) = F (0_{S})$
47	1 43	subm0	$⊢ X \in SubMnd (S) \to 0_{S} = 0_{U}$
48	47	adantl	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to 0_{S} = 0_{U}$
49	48	fveq2d	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to ({F ↾}_{X}) (0_{S}) = ({F ↾}_{X}) (0_{U})$
50		eqid	$⊢ 0_{T} = 0_{T}$
51	43 50	mhm0	$⊢ F \in (S MndHom T) \to F (0_{S}) = 0_{T}$
52	51	adantr	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to F (0_{S}) = 0_{T}$
53	46 49 52	3eqtr3d	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to ({F ↾}_{X}) (0_{U}) = 0_{T}$
54	15 42 53	3jca	$⊢ (F \in (S MndHom T) \land X \in SubMnd (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) \land ({F ↾}_{X}) (0_{U}) = 0_{T})$
55		eqid	$⊢ {Base}_{U} = {Base}_{U}$
56		eqid	$⊢ +_{U} = +_{U}$
57		eqid	$⊢ 0_{U} = 0_{U}$
58	55 6 56 23 57 50	ismhm	$⊢ {F ↾}_{X} \in (U MndHom T) \leftrightarrow ((U \in Mnd \land T \in Mnd) \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) \land ({F ↾}_{X}) (0_{U}) = 0_{T}))$
59	4 54 58	sylanbrc	$⊢ (F \in (S MndHom T) \land X \in SubMnd (S)) \to {F ↾}_{X} \in (U MndHom T)$

Metamath Proof Explorer

Theorem resmhm

Proof