Theorem subgsubm

Description: A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Assertion	subgsubm	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		subgrcl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
2		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
3	2	issubg3	⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑆 ) ) )
4	1 3	syl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑆 ) ) )
5	4	ibi	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝑆 ) )
6	5	simpld	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )