Theorem 0ringirng

Description: A zero ring R has no integral elements. (Contributed by Thierry Arnoux, 5-Feb-2025)

	Ref	Expression
Hypotheses	irngval.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
	irngval.u	$$⊢U=R{\upharpoonright }_{𝑠}S$$
	irngval.b	$$⊢B={\mathrm{Base}}_R$$
	irngval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	elirng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	elirng.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	0ringirng.1	$$⊢\phi \to \neg R\in \mathrm{NzRing}$$
Assertion	0ringirng	$$⊢\phi \to R\mathrm{IntgRing}S=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		irngval.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
2		irngval.u	$$⊢U=R{\upharpoonright }_{𝑠}S$$
3		irngval.b	$$⊢B={\mathrm{Base}}_R$$
4		irngval.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		elirng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		elirng.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
7		0ringirng.1	$$⊢\phi \to \neg R\in \mathrm{NzRing}$$
8		rex0	$$⊢\neg \exists p\in \varnothing O\left(p\right)\left(x\right)=\underset{\dot{}}{0}$$
9		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(U\right)={Monic}_{\mathrm{1p}}\left(U\right)$$
10		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
11	2	subrgring	$$⊢S\in \mathrm{SubRing}\left(R\right)\to U\in \mathrm{Ring}$$
12	6 11	syl	$$⊢\phi \to U\in \mathrm{Ring}$$
13	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
14	3	fveq2i	$$⊢\left|B\right|=\left|{\mathrm{Base}}_R\right|$$
15		0ringnnzr	$$⊢R\in \mathrm{Ring}\to \left(\left|{\mathrm{Base}}_R\right|=1\leftrightarrow \neg R\in \mathrm{NzRing}\right)$$
16	15	biimpar	$$⊢\left(R\in \mathrm{Ring}\wedge \neg R\in \mathrm{NzRing}\right)\to \left|{\mathrm{Base}}_R\right|=1$$
17	13 7 16	syl2anc	$$⊢\phi \to \left|{\mathrm{Base}}_R\right|=1$$
18	14 17	eqtrid	$$⊢\phi \to \left|B\right|=1$$
19	3	subrgss	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S\subseteq B$$
20	2 3	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_U$$
21	6 19 20	3syl	$$⊢\phi \to S={\mathrm{Base}}_U$$
22	21 6	eqeltrrd	$$⊢\phi \to {\mathrm{Base}}_U\in \mathrm{SubRing}\left(R\right)$$
23	3 13 18 22	0ringsubrg	$$⊢\phi \to \left|{\mathrm{Base}}_U\right|=1$$
24	9 10 12 23	0ringmon1p	$$⊢\phi \to {Monic}_{\mathrm{1p}}\left(U\right)=\varnothing$$
25	24	rexeqdv	$$⊢\phi \to \left(\exists p\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(p\right)\left(x\right)=\underset{\dot{}}{0}\leftrightarrow \exists p\in \varnothing O\left(p\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
26	8 25	mtbiri	$$⊢\phi \to \neg \exists p\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(p\right)\left(x\right)=\underset{\dot{}}{0}$$
27	1 2 3 4 5 6	elirng	$$⊢\phi \to \left(x\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \left(x\in B\wedge \exists p\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(p\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
28	27	simplbda	$$⊢\left(\phi \wedge x\in \left(R\mathrm{IntgRing}S\right)\right)\to \exists p\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(p\right)\left(x\right)=\underset{\dot{}}{0}$$
29	26 28	mtand	$$⊢\phi \to \neg x\in \left(R\mathrm{IntgRing}S\right)$$
30	29	eq0rdv	$$⊢\phi \to R\mathrm{IntgRing}S=\varnothing$$