Theorem rnglidl0

Description: Every non-unital ring contains a zero ideal. (Contributed by AV, 19-Feb-2025)

	Ref	Expression
Hypotheses	rnglidl0.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
	rnglidl0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	rnglidl0	$$⊢R\in \mathrm{Rng}\to \left\{\underset{\dot{}}{0}\right\}\in U$$

Proof

Step	Hyp	Ref	Expression
1		rnglidl0.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
2		rnglidl0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4	3 2	rng0cl	$$⊢R\in \mathrm{Rng}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
5	4	snssd	$$⊢R\in \mathrm{Rng}\to \left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_R$$
6	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
7	6	a1i	$$⊢R\in \mathrm{Rng}\to \underset{\dot{}}{0}\in \mathrm{V}$$
8	7	snn0d	$$⊢R\in \mathrm{Rng}\to \left\{\underset{\dot{}}{0}\right\}\ne \varnothing$$
9		eqid	$$⊢{\cdot }_R={\cdot }_R$$
10	3 9 2	rngrz	$$⊢\left(R\in \mathrm{Rng}\wedge x\in {\mathrm{Base}}_R\right)\to x{\cdot }_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
11	10	oveq1d	$$⊢\left(R\in \mathrm{Rng}\wedge x\in {\mathrm{Base}}_R\right)\to \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}{+}_R\underset{\dot{}}{0}$$
12		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
13	3 2	grpidcl	$$⊢R\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
14		eqid	$$⊢{+}_R={+}_R$$
15	3 14 2	grprid	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
16	12 13 15	syl2anc2	$$⊢R\in \mathrm{Rng}\to \underset{\dot{}}{0}{+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
17	16	adantr	$$⊢\left(R\in \mathrm{Rng}\wedge x\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
18	11 17	eqtrd	$$⊢\left(R\in \mathrm{Rng}\wedge x\in {\mathrm{Base}}_R\right)\to \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
19	6	elsn2	$$⊢\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
20	18 19	sylibr	$$⊢\left(R\in \mathrm{Rng}\wedge x\in {\mathrm{Base}}_R\right)\to \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
21		oveq2	$$⊢y=\underset{\dot{}}{0}\to x{\cdot }_{R}y=x{\cdot }_R\underset{\dot{}}{0}$$
22	21	oveq1d	$$⊢y=\underset{\dot{}}{0}\to \left(x{\cdot }_{R}y\right){+}_{R}z=\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z$$
23	22	eleq1d	$$⊢y=\underset{\dot{}}{0}\to \left(\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\right)$$
24	23	ralbidv	$$⊢y=\underset{\dot{}}{0}\to \left(\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\right)$$
25	6 24	ralsn	$$⊢\forall y\in \left\{\underset{\dot{}}{0}\right\}\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}$$
26		oveq2	$$⊢z=\underset{\dot{}}{0}\to \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z=\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}$$
27	26	eleq1d	$$⊢z=\underset{\dot{}}{0}\to \left(\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}\right)$$
28	6 27	ralsn	$$⊢\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
29	25 28	bitri	$$⊢\forall y\in \left\{\underset{\dot{}}{0}\right\}\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \left(x{\cdot }_R\underset{\dot{}}{0}\right){+}_R\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0}\right\}$$
30	20 29	sylibr	$$⊢\left(R\in \mathrm{Rng}\wedge x\in {\mathrm{Base}}_R\right)\to \forall y\in \left\{\underset{\dot{}}{0}\right\}\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}$$
31	30	ralrimiva	$$⊢R\in \mathrm{Rng}\to \forall x\in {\mathrm{Base}}_R\forall y\in \left\{\underset{\dot{}}{0}\right\}\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}$$
32	1 3 14 9	islidl	$$⊢\left\{\underset{\dot{}}{0}\right\}\in U\leftrightarrow \left(\left\{\underset{\dot{}}{0}\right\}\subseteq {\mathrm{Base}}_R\wedge \left\{\underset{\dot{}}{0}\right\}\ne \varnothing \wedge \forall x\in {\mathrm{Base}}_R\forall y\in \left\{\underset{\dot{}}{0}\right\}\forall z\in \left\{\underset{\dot{}}{0}\right\}\left(x{\cdot }_{R}y\right){+}_{R}z\in \left\{\underset{\dot{}}{0}\right\}\right)$$
33	5 8 31 32	syl3anbrc	$$⊢R\in \mathrm{Rng}\to \left\{\underset{\dot{}}{0}\right\}\in U$$