Theorem grpmnd

Description: A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Assertion	grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
3		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
4	1 2 3	isgrp	⊢ ( 𝐺 ∈ Grp ↔ ( 𝐺 ∈ Mnd ∧ ∀ 𝑎 ∈ ( Base ‘ 𝐺 ) ∃ 𝑚 ∈ ( Base ‘ 𝐺 ) ( 𝑚 ( +g ‘ 𝐺 ) 𝑎 ) = ( 0g ‘ 𝐺 ) ) )
5	4	simplbi	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )