Theorem ress0gOLD

Description: Obsolete version of ress0g as of 12-Aug-2026. 0g is unaffected by restriction. This is a bit more generic than submnd0 . (Contributed by Thierry Arnoux, 23-Oct-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ress0g.s	$$⊢S=R{\upharpoonright }_{𝑠}A$$
	ress0g.b	$$⊢B={\mathrm{Base}}_R$$
	ress0g.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	ress0gOLD	$$⊢\left(R\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in A\wedge A\subseteq B\right)\to \underset{\dot{}}{0}=0_S$$

Proof

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