Theorem isrprm

Description: Property for P to be a prime element in the ring R . (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	isrprm.1	$$⊢B={\mathrm{Base}}_R$$
	isrprm.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
	isrprm.3	$$⊢\underset{\dot{}}{0}=0_R$$
	isrprm.4	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	isrprm.5	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	isrprm	$$⊢R\in V\to \left(P\in \mathrm{RPrime}\left(R\right)\leftrightarrow \left(P\in \left(B\setminus \left(U\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(P\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(P\underset{\dot{}}{\parallel }x\vee P\underset{\dot{}}{\parallel }y\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isrprm.1	$$⊢B={\mathrm{Base}}_R$$
2		isrprm.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		isrprm.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		isrprm.4	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
5		isrprm.5	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6	1 2 3 5 4	rprmval	$$⊢R\in V\to \mathrm{RPrime}\left(R\right)=\left\{p\in \left(B\setminus \left(U\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)|\forall x\in B\forall y\in B\left(p\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(p\underset{\dot{}}{\parallel }x\vee p\underset{\dot{}}{\parallel }y\right)\right)\right\}$$
7	6	eleq2d	$$⊢R\in V\to \left(P\in \mathrm{RPrime}\left(R\right)\leftrightarrow P\in \left\{p\in \left(B\setminus \left(U\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)|\forall x\in B\forall y\in B\left(p\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(p\underset{\dot{}}{\parallel }x\vee p\underset{\dot{}}{\parallel }y\right)\right)\right\}\right)$$
8		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\leftrightarrow P\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\right)$$
9		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\parallel }x\leftrightarrow P\underset{\dot{}}{\parallel }x\right)$$
10		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\parallel }y\leftrightarrow P\underset{\dot{}}{\parallel }y\right)$$
11	9 10	orbi12d	$$⊢p=P\to \left(\left(p\underset{\dot{}}{\parallel }x\vee p\underset{\dot{}}{\parallel }y\right)\leftrightarrow \left(P\underset{\dot{}}{\parallel }x\vee P\underset{\dot{}}{\parallel }y\right)\right)$$
12	8 11	imbi12d	$$⊢p=P\to \left(\left(p\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(p\underset{\dot{}}{\parallel }x\vee p\underset{\dot{}}{\parallel }y\right)\right)\leftrightarrow \left(P\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(P\underset{\dot{}}{\parallel }x\vee P\underset{\dot{}}{\parallel }y\right)\right)\right)$$
13	12	2ralbidv	$$⊢p=P\to \left(\forall x\in B\forall y\in B\left(p\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(p\underset{\dot{}}{\parallel }x\vee p\underset{\dot{}}{\parallel }y\right)\right)\leftrightarrow \forall x\in B\forall y\in B\left(P\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(P\underset{\dot{}}{\parallel }x\vee P\underset{\dot{}}{\parallel }y\right)\right)\right)$$
14	13	elrab	$$⊢P\in \left\{p\in \left(B\setminus \left(U\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)|\forall x\in B\forall y\in B\left(p\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(p\underset{\dot{}}{\parallel }x\vee p\underset{\dot{}}{\parallel }y\right)\right)\right\}\leftrightarrow \left(P\in \left(B\setminus \left(U\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(P\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(P\underset{\dot{}}{\parallel }x\vee P\underset{\dot{}}{\parallel }y\right)\right)\right)$$
15	7 14	syl6bb	$$⊢R\in V\to \left(P\in \mathrm{RPrime}\left(R\right)\leftrightarrow \left(P\in \left(B\setminus \left(U\cup \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall x\in B\forall y\in B\left(P\underset{\dot{}}{\parallel }\left(x\underset{\dot{}}{·}y\right)\to \left(P\underset{\dot{}}{\parallel }x\vee P\underset{\dot{}}{\parallel }y\right)\right)\right)\right)$$