Metamath Proof Explorer


Theorem ghmmhm

Description: A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion ghmmhm ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 ghmgrp1 ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
2 1 grpmndd ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Mnd )
3 ghmgrp2 ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
4 3 grpmndd ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Mnd )
5 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
7 5 6 ghmf ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
8 eqid ( +g𝑆 ) = ( +g𝑆 )
9 eqid ( +g𝑇 ) = ( +g𝑇 )
10 5 8 9 ghmlin ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
11 10 3expb ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
12 11 ralrimivva ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) )
13 eqid ( 0g𝑆 ) = ( 0g𝑆 )
14 eqid ( 0g𝑇 ) = ( 0g𝑇 )
15 13 14 ghmid ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) )
16 7 12 15 3jca ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) ) )
17 5 6 8 9 13 14 ismhm ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ↔ ( ( 𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( 𝐹 ‘ ( 𝑥 ( +g𝑆 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑇 ) ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g𝑆 ) ) = ( 0g𝑇 ) ) ) )
18 2 4 16 17 syl21anbrc ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )