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

Metamath Proof Explorer

Theorem subm0cl

Description: Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis subm0cl.z ⊢ 0 = ( 0g ‘ 𝑀 )
Assertion subm0cl ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 0 ∈ 𝑆 )

Proof

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