mhmco

Description: The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

		Ref	Expression
	Assertion	mhmco	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to F \circ G \in (S MndHom U)$

Proof

Step	Hyp	Ref	Expression
1		mhmrcl2	$⊢ F \in (T MndHom U) \to U \in Mnd$
2		mhmrcl1	$⊢ G \in (S MndHom T) \to S \in Mnd$
3	1 2	anim12ci	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to (S \in Mnd \land U \in Mnd)$
4		eqid	$⊢ {Base}_{T} = {Base}_{T}$
5		eqid	$⊢ {Base}_{U} = {Base}_{U}$
6	4 5	mhmf	$⊢ F \in (T MndHom U) \to F : {Base}_{T} ⟶ {Base}_{U}$
7		eqid	$⊢ {Base}_{S} = {Base}_{S}$
8	7 4	mhmf	$⊢ G \in (S MndHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
9		fco	$⊢ (F : {Base}_{T} ⟶ {Base}_{U} \land G : {Base}_{S} ⟶ {Base}_{T}) \to (F \circ G) : {Base}_{S} ⟶ {Base}_{U}$
10	6 8 9	syl2an	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to (F \circ G) : {Base}_{S} ⟶ {Base}_{U}$
11		eqid	$⊢ +_{S} = +_{S}$
12		eqid	$⊢ +_{T} = +_{T}$
13	7 11 12	mhmlin	$⊢ (G \in (S MndHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to G (x +_{S} y) = G (x) +_{T} G (y)$
14	13	3expb	$⊢ (G \in (S MndHom T) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (x +_{S} y) = G (x) +_{T} G (y)$
15	14	adantll	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (x +_{S} y) = G (x) +_{T} G (y)$
16	15	fveq2d	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (G (x +_{S} y)) = F (G (x) +_{T} G (y))$
17		simpll	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F \in (T MndHom U)$
18	8	ad2antlr	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G : {Base}_{S} ⟶ {Base}_{T}$
19		simprl	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to x \in {Base}_{S}$
20	18 19	ffvelrnd	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (x) \in {Base}_{T}$
21		simprr	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to y \in {Base}_{S}$
22	18 21	ffvelrnd	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (y) \in {Base}_{T}$
23		eqid	$⊢ +_{U} = +_{U}$
24	4 12 23	mhmlin	$⊢ (F \in (T MndHom U) \land G (x) \in {Base}_{T} \land G (y) \in {Base}_{T}) \to F (G (x) +_{T} G (y)) = F (G (x)) +_{U} F (G (y))$
25	17 20 22 24	syl3anc	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (G (x) +_{T} G (y)) = F (G (x)) +_{U} F (G (y))$
26	16 25	eqtrd	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (G (x +_{S} y)) = F (G (x)) +_{U} F (G (y))$
27	2	adantl	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to S \in Mnd$
28	7 11	mndcl	$⊢ (S \in Mnd \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
29	28	3expb	$⊢ (S \in Mnd \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to x +_{S} y \in {Base}_{S}$
30	27 29	sylan	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to x +_{S} y \in {Base}_{S}$
31		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land x +_{S} y \in {Base}_{S}) \to (F \circ G) (x +_{S} y) = F (G (x +_{S} y))$
32	18 30 31	syl2anc	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (x +_{S} y) = F (G (x +_{S} y))$
33		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land x \in {Base}_{S}) \to (F \circ G) (x) = F (G (x))$
34	18 19 33	syl2anc	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (x) = F (G (x))$
35		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land y \in {Base}_{S}) \to (F \circ G) (y) = F (G (y))$
36	18 21 35	syl2anc	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (y) = F (G (y))$
37	34 36	oveq12d	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (x) +_{U} (F \circ G) (y) = F (G (x)) +_{U} F (G (y))$
38	26 32 37	3eqtr4d	$⊢ ((F \in (T MndHom U) \land G \in (S MndHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (x +_{S} y) = (F \circ G) (x) +_{U} (F \circ G) (y)$
39	38	ralrimivva	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to \forall x \in {Base}_{S} \forall y \in {Base}_{S} (F \circ G) (x +_{S} y) = (F \circ G) (x) +_{U} (F \circ G) (y)$
40	8	adantl	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to G : {Base}_{S} ⟶ {Base}_{T}$
41		eqid	$⊢ 0_{S} = 0_{S}$
42	7 41	mndidcl	$⊢ S \in Mnd \to 0_{S} \in {Base}_{S}$
43	27 42	syl	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to 0_{S} \in {Base}_{S}$
44		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land 0_{S} \in {Base}_{S}) \to (F \circ G) (0_{S}) = F (G (0_{S}))$
45	40 43 44	syl2anc	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to (F \circ G) (0_{S}) = F (G (0_{S}))$
46		eqid	$⊢ 0_{T} = 0_{T}$
47	41 46	mhm0	$⊢ G \in (S MndHom T) \to G (0_{S}) = 0_{T}$
48	47	adantl	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to G (0_{S}) = 0_{T}$
49	48	fveq2d	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to F (G (0_{S})) = F (0_{T})$
50		eqid	$⊢ 0_{U} = 0_{U}$
51	46 50	mhm0	$⊢ F \in (T MndHom U) \to F (0_{T}) = 0_{U}$
52	51	adantr	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to F (0_{T}) = 0_{U}$
53	45 49 52	3eqtrd	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to (F \circ G) (0_{S}) = 0_{U}$
54	10 39 53	3jca	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to ((F \circ G) : {Base}_{S} ⟶ {Base}_{U} \land \forall x \in {Base}_{S} \forall y \in {Base}_{S} (F \circ G) (x +_{S} y) = (F \circ G) (x) +_{U} (F \circ G) (y) \land (F \circ G) (0_{S}) = 0_{U})$
55	7 5 11 23 41 50	ismhm	$⊢ F \circ G \in (S MndHom U) \leftrightarrow ((S \in Mnd \land U \in Mnd) \land ((F \circ G) : {Base}_{S} ⟶ {Base}_{U} \land \forall x \in {Base}_{S} \forall y \in {Base}_{S} (F \circ G) (x +_{S} y) = (F \circ G) (x) +_{U} (F \circ G) (y) \land (F \circ G) (0_{S}) = 0_{U}))$
56	3 54 55	sylanbrc	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to F \circ G \in (S MndHom U)$

Metamath Proof Explorer

Theorem mhmco

Proof