Metamath Proof Explorer


Theorem mgmhmco

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

Ref Expression
Assertion mgmhmco F T MgmHom U G S MgmHom T F G S MgmHom U

Proof

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