Theorem rprmnunit

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

	Ref	Expression
Hypotheses	rprmdvds.2	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmdvds.3	$$⊢U=\mathrm{Unit}\left(R\right)$$
	rprmdvds.5	$$⊢\phi \to R\in V$$
	rprmdvds.6	$$⊢\phi \to Q\in P$$
Assertion	rprmnunit	$$⊢\phi \to \neg Q\in U$$

Proof

Step	Hyp	Ref	Expression
1		rprmdvds.2	$$⊢P=\mathrm{RPrime}\left(R\right)$$
2		rprmdvds.3	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		rprmdvds.5	$$⊢\phi \to R\in V$$
4		rprmdvds.6	$$⊢\phi \to Q\in P$$
5		eqidd	$$⊢\phi \to U\cup \left\{0_R\right\}=U\cup \left\{0_R\right\}$$
6	4 1	eleqtrdi	$$⊢\phi \to Q\in \mathrm{RPrime}\left(R\right)$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8		eqid	$$⊢0_R=0_R$$
9		eqid	$$⊢{\parallel }_r\left(R\right)={\parallel }_r\left(R\right)$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11	7 2 8 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(U\cup \left\{0_R\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(U\cup \left\{0_R\right\}\right)\right)$$
13	3 6 12	syl2anc	$$⊢\phi \to Q\in \left({\mathrm{Base}}_R\setminus \left(U\cup \left\{0_R\right\}\right)\right)$$
14	13	eldifbd	$$⊢\phi \to \neg Q\in \left(U\cup \left\{0_R\right\}\right)$$
15		nelun	$$⊢U\cup \left\{0_R\right\}=U\cup \left\{0_R\right\}\to \left(\neg Q\in \left(U\cup \left\{0_R\right\}\right)\leftrightarrow \left(\neg Q\in U\wedge \neg Q\in \left\{0_R\right\}\right)\right)$$
16	15	simprbda	$$⊢\left(U\cup \left\{0_R\right\}=U\cup \left\{0_R\right\}\wedge \neg Q\in \left(U\cup \left\{0_R\right\}\right)\right)\to \neg Q\in U$$
17	5 14 16	syl2anc	$$⊢\phi \to \neg Q\in U$$