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

Metamath Proof Explorer

Theorem ghmmhmb

Description: Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion ghmmhmb ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 ghmmhm ⊢ ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) )
2 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
3 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
4 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
5 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
6 simpll ⊢ ( ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑆 ∈ Grp )
7 simplr ⊢ ( ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑇 ∈ Grp )
8 2 3 mhmf ⊢ ( 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑓 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
9 8 adantl ⊢ ( ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑓 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
10 2 4 5 mhmlin ⊢ ( ( 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝑓 ‘ 𝑦 ) ) )
11 10 3expb ⊢ ( ( 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝑓 ‘ 𝑦 ) ) )
12 11 adantll ⊢ ( ( ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝑓 ‘ 𝑦 ) ) )
13 2 3 4 5 6 7 9 12 isghmd ⊢ ( ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) ∧ 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) )
14 13 ex ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ) )
15 1 14 impbid2 ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑓 ∈ ( 𝑆 GrpHom 𝑇 ) ↔ 𝑓 ∈ ( 𝑆 MndHom 𝑇 ) ) )
16 15 eqrdv ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑇 ∈ Grp ) → ( 𝑆 GrpHom 𝑇 ) = ( 𝑆 MndHom 𝑇 ) )