Theorem rprmnz

Description: A ring prime is nonzero. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmnz.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmnz.0	$$⊢\underset{\dot{}}{0}=0_R$$
	rprmnz.r	$$⊢\phi \to R\in V$$
	rprmnz.q	$$⊢\phi \to Q\in P$$
Assertion	rprmnz	$$⊢\phi \to Q\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		rprmnz.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
2		rprmnz.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		rprmnz.r	$$⊢\phi \to R\in V$$
4		rprmnz.q	$$⊢\phi \to Q\in P$$
5		eqidd	$$⊢\phi \to \mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}$$
6	4 1	eleqtrdi	$$⊢\phi \to Q\in \mathrm{RPrime}\left(R\right)$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
9		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11	7 8 2 9 10	isrprm	$$⊢R\in V\to \left(Q\in \mathrm{RPrime}\left(R\right)\leftrightarrow \left(Q\in \left({\mathrm{Base}}_R\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R\left(Q{\parallel }_r\left(R\right)\left(x{\cdot }_{R}y\right)\to \left(Q{\parallel }_r\left(R\right)x\vee Q{\parallel }_r\left(R\right)y\right)\right)\right)\right)$$
12	11	simprbda	$$⊢\left(R\in V\wedge Q\in \mathrm{RPrime}\left(R\right)\right)\to Q\in \left({\mathrm{Base}}_R\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
13	3 6 12	syl2anc	$$⊢\phi \to Q\in \left({\mathrm{Base}}_R\setminus \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
14	13	eldifbd	$$⊢\phi \to \neg Q\in \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)$$
15		nelun	$$⊢\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\to \left(\neg Q\in \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(\neg Q\in \mathrm{Unit}\left(R\right)\wedge \neg Q\in \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
16	15	simplbda	$$⊢\left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\wedge \neg Q\in \left(\mathrm{Unit}\left(R\right)\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \neg Q\in \left\{\underset{\dot{}}{0}\right\}$$
17	5 14 16	syl2anc	$$⊢\phi \to \neg Q\in \left\{\underset{\dot{}}{0}\right\}$$
18		elsng	$$⊢Q\in P\to \left(Q\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow Q=\underset{\dot{}}{0}\right)$$
19	4 18	syl	$$⊢\phi \to \left(Q\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow Q=\underset{\dot{}}{0}\right)$$
20	19	necon3bbid	$$⊢\phi \to \left(\neg Q\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow Q\ne \underset{\dot{}}{0}\right)$$
21	17 20	mpbid	$$⊢\phi \to Q\ne \underset{\dot{}}{0}$$