This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑇 ) )