Theorem subm0

Description: Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	submmnd.h	⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
	subm0.z	⊢ 0 = ( 0g ‘ 𝑀 )
Assertion	subm0	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 0 = ( 0g ‘ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		submmnd.h	⊢ 𝐻 = ( 𝑀 ↾s 𝑆 )
2		subm0.z	⊢ 0 = ( 0g ‘ 𝑀 )
3		submrcl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )
4	1	submmnd	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝐻 ∈ Mnd )
5		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
6	5	submss	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
7	2	subm0cl	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 0 ∈ 𝑆 )
8	5 2 1	submnd0	⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐻 ∈ Mnd ) ∧ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ 0 ∈ 𝑆 ) ) → 0 = ( 0g ‘ 𝐻 ) )
9	3 4 6 7 8	syl22anc	⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 0 = ( 0g ‘ 𝐻 ) )