Theorem ress0g

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

	Ref	Expression
Hypotheses	ress0g.s	$$⊢S=R{\upharpoonright }_{𝑠}A$$
	ress0g.b	$$⊢B={\mathrm{Base}}_R$$
	ress0g.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	ress0g	$$⊢\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		eqid	$$⊢{+}_R={+}_R$$
5	2 4	mndid	$$⊢R\in \mathrm{Mnd}\to \exists u\in B\forall x\in B\left(u{+}_{R}x=x\wedge x{+}_{R}u=x\right)$$
6	5	3ad2ant1	$$⊢\left(R\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in A\wedge A\subseteq B\right)\to \exists u\in B\forall x\in B\left(u{+}_{R}x=x\wedge x{+}_{R}u=x\right)$$
7		simp3	$$⊢\left(R\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in A\wedge A\subseteq B\right)\to A\subseteq B$$
8		simp2	$$⊢\left(R\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in A\wedge A\subseteq B\right)\to \underset{\dot{}}{0}\in A$$
9	2 4 3 6 1 7 8	idressid	$$⊢\left(R\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in A\wedge A\subseteq B\right)\to 0_S=\underset{\dot{}}{0}$$
10	9	eqcomd	$$⊢\left(R\in \mathrm{Mnd}\wedge \underset{\dot{}}{0}\in A\wedge A\subseteq B\right)\to \underset{\dot{}}{0}=0_S$$