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

Metamath Proof Explorer

Theorem submmnd

Description: Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis submmnd.h ⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
Assertion submmnd ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝐻 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 submmnd.h ⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
2 submrcl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )
3 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
5 3 4 1 issubm2 ⊢ ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ∧ 𝐻 ∈ Mnd ) ) )
6 2 5 syl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ∧ 𝐻 ∈ Mnd ) ) )
7 6 ibi ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ∧ 𝐻 ∈ Mnd ) )
8 7 simp3d ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝐻 ∈ Mnd )