submnd0

Description: The zero of a submonoid is the same as the zero in the parent monoid. (Note that we must add the condition that the zero of the parent monoid is actually contained in the submonoid, because it is possible to have "subsets that are monoids" which are not submonoids because they have a different identity element. See, for example, smndex1mnd and smndex1n0mnd ). (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	submnd0.b	$⊢ B = {Base}_{G}$
	submnd0.z	$⊢ \underset{˙}{0} = 0_{G}$
	submnd0.h	$⊢ H = G ↾_{𝑠} S$
Assertion	submnd0	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to \underset{˙}{0} = 0_{H}$

Proof

Step	Hyp	Ref	Expression
1		submnd0.b	$⊢ B = {Base}_{G}$
2		submnd0.z	$⊢ \underset{˙}{0} = 0_{G}$
3		submnd0.h	$⊢ H = G ↾_{𝑠} S$
4		eqid	$⊢ {Base}_{H} = {Base}_{H}$
5		eqid	$⊢ 0_{H} = 0_{H}$
6		eqid	$⊢ +_{H} = +_{H}$
7		simprr	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to \underset{˙}{0} \in S$
8	3 1	ressbas2	$⊢ S \subseteq B \to S = {Base}_{H}$
9	8	ad2antrl	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to S = {Base}_{H}$
10	7 9	eleqtrd	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to \underset{˙}{0} \in {Base}_{H}$
11		fvex	$⊢ {Base}_{H} \in V$
12	9 11	eqeltrdi	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to S \in V$
13	12	adantr	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to S \in V$
14		eqid	$⊢ +_{G} = +_{G}$
15	3 14	ressplusg	$⊢ S \in V \to +_{G} = +_{H}$
16	13 15	syl	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to +_{G} = +_{H}$
17	16	oveqd	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to \underset{˙}{0} +_{G} x = \underset{˙}{0} +_{H} x$
18		simpll	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to G \in Mnd$
19	3 1	ressbasss	$⊢ {Base}_{H} \subseteq B$
20	19	sseli	$⊢ x \in {Base}_{H} \to x \in B$
21	1 14 2	mndlid	$⊢ (G \in Mnd \land x \in B) \to \underset{˙}{0} +_{G} x = x$
22	18 20 21	syl2an	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to \underset{˙}{0} +_{G} x = x$
23	17 22	eqtr3d	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to \underset{˙}{0} +_{H} x = x$
24	16	oveqd	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to x +_{G} \underset{˙}{0} = x +_{H} \underset{˙}{0}$
25	1 14 2	mndrid	$⊢ (G \in Mnd \land x \in B) \to x +_{G} \underset{˙}{0} = x$
26	18 20 25	syl2an	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to x +_{G} \underset{˙}{0} = x$
27	24 26	eqtr3d	$⊢ (((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \land x \in {Base}_{H}) \to x +_{H} \underset{˙}{0} = x$
28	4 5 6 10 23 27	ismgmid2	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \to \underset{˙}{0} = 0_{H}$

Metamath Proof Explorer

Theorem submnd0

Proof