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