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 e. ( T MgmHom U ) /\ G e. ( S MgmHom T ) ) -> ( F o. G ) e. ( S MgmHom U ) )

Proof

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