subm0

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

Step	Hyp	Ref	Expression
1		submmnd.h	$⊢ H = M ↾_{𝑠} S$
2		subm0.z	$⊢ \underset{˙}{0} = 0_{M}$
3		submrcl	$⊢ S \in SubMnd (M) \to M \in Mnd$
4	1	submmnd	$⊢ S \in SubMnd (M) \to H \in Mnd$
5		eqid	$⊢ {Base}_{M} = {Base}_{M}$
6	5	submss	$⊢ S \in SubMnd (M) \to S \subseteq {Base}_{M}$
7	2	subm0cl	$⊢ S \in SubMnd (M) \to \underset{˙}{0} \in S$
8	5 2 1	submnd0	$⊢ ((M \in Mnd \land H \in Mnd) \land (S \subseteq {Base}_{M} \land \underset{˙}{0} \in S)) \to \underset{˙}{0} = 0_{H}$
9	3 4 6 7 8	syl22anc	$⊢ S \in SubMnd (M) \to \underset{˙}{0} = 0_{H}$

Metamath Proof Explorer