mgmhmco

Description: The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		mgmhmrcl	$⊢ F \in (T MgmHom U) \to (T \in Mgm \land U \in Mgm)$
2	1	simprd	$⊢ F \in (T MgmHom U) \to U \in Mgm$
3		mgmhmrcl	$⊢ G \in (S MgmHom T) \to (S \in Mgm \land T \in Mgm)$
4	3	simpld	$⊢ G \in (S MgmHom T) \to S \in Mgm$
5	2 4	anim12ci	$⊢ (F \in (T MgmHom U) \land G \in (S MgmHom T)) \to (S \in Mgm \land U \in Mgm)$
6		eqid	$⊢ {Base}_{T} = {Base}_{T}$
7		eqid	$⊢ {Base}_{U} = {Base}_{U}$
8	6 7	mgmhmf	$⊢ F \in (T MgmHom U) \to F : {Base}_{T} ⟶ {Base}_{U}$
9		eqid	$⊢ {Base}_{S} = {Base}_{S}$
10	9 6	mgmhmf	$⊢ G \in (S MgmHom T) \to G : {Base}_{S} ⟶ {Base}_{T}$
11		fco	$⊢ (F : {Base}_{T} ⟶ {Base}_{U} \land G : {Base}_{S} ⟶ {Base}_{T}) \to (F \circ G) : {Base}_{S} ⟶ {Base}_{U}$
12	8 10 11	syl2an	$⊢ (F \in (T MgmHom U) \land G \in (S MgmHom T)) \to (F \circ G) : {Base}_{S} ⟶ {Base}_{U}$
13		eqid	$⊢ +_{S} = +_{S}$
14		eqid	$⊢ +_{T} = +_{T}$
15	9 13 14	mgmhmlin	$⊢ (G \in (S MgmHom T) \land x \in {Base}_{S} \land y \in {Base}_{S}) \to G (x +_{S} y) = G (x) +_{T} G (y)$
16	15	3expb	$⊢ (G \in (S MgmHom T) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (x +_{S} y) = G (x) +_{T} G (y)$
17	16	adantll	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (x +_{S} y) = G (x) +_{T} G (y)$
18	17	fveq2d	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (G (x +_{S} y)) = F (G (x) +_{T} G (y))$
19		simpll	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F \in (T MgmHom U)$
20	10	ad2antlr	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G : {Base}_{S} ⟶ {Base}_{T}$
21		simprl	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to x \in {Base}_{S}$
22	20 21	ffvelrnd	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (x) \in {Base}_{T}$
23		simprr	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to y \in {Base}_{S}$
24	20 23	ffvelrnd	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to G (y) \in {Base}_{T}$
25		eqid	$⊢ +_{U} = +_{U}$
26	6 14 25	mgmhmlin	$⊢ (F \in (T MgmHom 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))$
27	19 22 24 26	syl3anc	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom 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))$
28	18 27	eqtrd	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to F (G (x +_{S} y)) = F (G (x)) +_{U} F (G (y))$
29	4	adantl	$⊢ (F \in (T MgmHom U) \land G \in (S MgmHom T)) \to S \in Mgm$
30	9 13	mgmcl	$⊢ (S \in Mgm \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
31	30	3expb	$⊢ (S \in Mgm \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to x +_{S} y \in {Base}_{S}$
32	29 31	sylan	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to x +_{S} y \in {Base}_{S}$
33		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))$
34	20 32 33	syl2anc	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (x +_{S} y) = F (G (x +_{S} y))$
35		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land x \in {Base}_{S}) \to (F \circ G) (x) = F (G (x))$
36	20 21 35	syl2anc	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (x) = F (G (x))$
37		fvco3	$⊢ (G : {Base}_{S} ⟶ {Base}_{T} \land y \in {Base}_{S}) \to (F \circ G) (y) = F (G (y))$
38	20 23 37	syl2anc	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom T)) \land (x \in {Base}_{S} \land y \in {Base}_{S})) \to (F \circ G) (y) = F (G (y))$
39	36 38	oveq12d	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom 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))$
40	28 34 39	3eqtr4d	$⊢ ((F \in (T MgmHom U) \land G \in (S MgmHom 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)$
41	40	ralrimivva	$⊢ (F \in (T MgmHom U) \land G \in (S MgmHom 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)$
42	12 41	jca	$⊢ (F \in (T MgmHom U) \land G \in (S MgmHom 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))$
43	9 7 13 25	ismgmhm	$⊢ F \circ G \in (S MgmHom U) \leftrightarrow ((S \in Mgm \land U \in Mgm) \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)))$
44	5 42 43	sylanbrc	$⊢ (F \in (T MgmHom U) \land G \in (S MgmHom T)) \to F \circ G \in (S MgmHom U)$

Metamath Proof Explorer

Theorem mgmhmco

Proof