ress0g

Description: 0g is unaffected by restriction. This is a bit more generic than submnd0 . (Contributed by Thierry Arnoux, 23-Oct-2017)

	Ref	Expression
Hypotheses	ress0g.s	$⊢ S = R ↾_{𝑠} A$
	ress0g.b	$⊢ B = {Base}_{R}$
	ress0g.0	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	ress0g	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to \underset{˙}{0} = 0_{S}$

Proof

Step	Hyp	Ref	Expression
1		ress0g.s	$⊢ S = R ↾_{𝑠} A$
2		ress0g.b	$⊢ B = {Base}_{R}$
3		ress0g.0	$⊢ \underset{˙}{0} = 0_{R}$
4	1 2	ressbas2	$⊢ A \subseteq B \to A = {Base}_{S}$
5	4	3ad2ant3	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to A = {Base}_{S}$
6		simp3	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to A \subseteq B$
7	2	fvexi	$⊢ B \in V$
8		ssexg	$⊢ (A \subseteq B \land B \in V) \to A \in V$
9	6 7 8	sylancl	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to A \in V$
10		eqid	$⊢ +_{R} = +_{R}$
11	1 10	ressplusg	$⊢ A \in V \to +_{R} = +_{S}$
12	9 11	syl	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to +_{R} = +_{S}$
13		simp2	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to \underset{˙}{0} \in A$
14		simpl1	$⊢ ((R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \land x \in A) \to R \in Mnd$
15	6	sselda	$⊢ ((R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \land x \in A) \to x \in B$
16	2 10 3	mndlid	$⊢ (R \in Mnd \land x \in B) \to \underset{˙}{0} +_{R} x = x$
17	14 15 16	syl2anc	$⊢ ((R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \land x \in A) \to \underset{˙}{0} +_{R} x = x$
18	2 10 3	mndrid	$⊢ (R \in Mnd \land x \in B) \to x +_{R} \underset{˙}{0} = x$
19	14 15 18	syl2anc	$⊢ ((R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \land x \in A) \to x +_{R} \underset{˙}{0} = x$
20	5 12 13 17 19	grpidd	$⊢ (R \in Mnd \land \underset{˙}{0} \in A \land A \subseteq B) \to \underset{˙}{0} = 0_{S}$

Metamath Proof Explorer

Theorem ress0g

Proof