Metamath Proof Explorer

Theorem mgmhmco

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

Ref Expression
Assertion mgmhmco ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MgmHom 𝑈 ) )

Proof

Step Hyp Ref Expression
1 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) → ( 𝑇 ∈ Mgm ∧ 𝑈 ∈ Mgm ) )
2 1 simprd ⊢ ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) → 𝑈 ∈ Mgm )
3 mgmhmrcl ⊢ ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
4 3 simpld ⊢ ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝑆 ∈ Mgm )
5 2 4 anim12ci ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm ) )
6 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
7 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
8 6 7 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) → 𝐹 : ( Base ‘ 𝑇 ) ⟶ ( Base ‘ 𝑈 ) )
9 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 9 6 mgmhmf ⊢ ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
11 fco ⊢ ( ( 𝐹 : ( Base ‘ 𝑇 ) ⟶ ( Base ‘ 𝑈 ) ∧ 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
12 8 10 11 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
13 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
14 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
15 9 13 14 mgmhmlin ⊢ ( ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
16 15 3expb ⊢ ( ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
17 16 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
18 17 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) ) )
19 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) )
20 10 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
21 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
22 20 21 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
23 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
24 20 23 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
25 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
26 6 14 25 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
27 19 22 24 26 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
28 18 27 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
29 4 adantl ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝑆 ∈ Mgm )
30 9 13 mgmcl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
31 30 3expb ⊢ ( ( 𝑆 ∈ Mgm ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
32 29 31 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
33 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
34 20 32 33 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
35 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
36 20 21 35 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
37 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
38 20 23 37 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
39 36 38 oveq12d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
40 28 34 39 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
41 40 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
42 12 41 jca ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ) )
43 9 7 13 25 ismgmhm ⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MgmHom 𝑈 ) ↔ ( ( 𝑆 ∈ Mgm ∧ 𝑈 ∈ Mgm ) ∧ ( ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ) ) )
44 5 42 43 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑇 MgmHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MgmHom 𝑈 ) )