Metamath Proof Explorer

Theorem mhmco

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

Ref Expression
Assertion mhmco ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MndHom 𝑈 ) )

Proof

Step Hyp Ref Expression
1 mhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) → 𝑈 ∈ Mnd )
2 mhmrcl1 ⊢ ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd )
3 1 2 anim12ci ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝑆 ∈ Mnd ∧ 𝑈 ∈ Mnd ) )
4 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
5 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
6 4 5 mhmf ⊢ ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) → 𝐹 : ( Base ‘ 𝑇 ) ⟶ ( Base ‘ 𝑈 ) )
7 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 7 4 mhmf ⊢ ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
9 fco ⊢ ( ( 𝐹 : ( Base ‘ 𝑇 ) ⟶ ( Base ‘ 𝑈 ) ∧ 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
10 6 8 9 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) )
11 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
12 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
13 7 11 12 mhmlin ⊢ ( ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
14 13 3expb ⊢ ( ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
15 14 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
16 15 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) ) )
17 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) )
18 8 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
19 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
20 18 19 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) )
21 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
22 18 21 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
23 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
24 4 12 23 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
25 17 20 22 24 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
26 16 25 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
27 2 adantl ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑆 ∈ Mnd )
28 7 11 mndcl ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
29 28 3expb ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
30 27 29 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
31 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
32 18 30 31 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
33 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
34 18 19 33 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
35 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
36 18 21 35 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
37 34 36 oveq12d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
38 26 32 37 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
39 38 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
40 8 adantl ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
41 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
42 7 41 mndidcl ⊢ ( 𝑆 ∈ Mnd → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
43 27 42 syl ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
44 fvco3 ⊢ ( ( 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 0g ‘ 𝑆 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) ) )
45 40 43 44 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 0g ‘ 𝑆 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) ) )
46 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
47 41 46 mhm0 ⊢ ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
48 47 adantl ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
49 48 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑇 ) ) )
50 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
51 46 50 mhm0 ⊢ ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) → ( 𝐹 ‘ ( 0g ‘ 𝑇 ) ) = ( 0g ‘ 𝑈 ) )
52 51 adantr ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑇 ) ) = ( 0g ‘ 𝑈 ) )
53 45 49 52 3eqtrd ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑈 ) )
54 10 39 53 3jca ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑈 ) ) )
55 7 5 11 23 41 50 ismhm ⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MndHom 𝑈 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑈 ∈ Mnd ) ∧ ( ( 𝐹 ∘ 𝐺 ) : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝑈 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ∧ ( ( 𝐹 ∘ 𝐺 ) ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑈 ) ) ) )
56 3 54 55 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MndHom 𝑈 ) )