Theorem isufd

Description: The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypotheses	isufd.i	$$⊢I=\mathrm{PrmIdeal}\left(R\right)$$
	isufd.3	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	isufd.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	isufd	$$⊢R\in \mathrm{UFD}\leftrightarrow \left(R\in \mathrm{IDomn}\wedge \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		isufd.i	$$⊢I=\mathrm{PrmIdeal}\left(R\right)$$
2		isufd.3	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		isufd.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		fveq2	$$⊢r=R\to \mathrm{PrmIdeal}\left(r\right)=\mathrm{PrmIdeal}\left(R\right)$$
5	4 1	eqtr4di	$$⊢r=R\to \mathrm{PrmIdeal}\left(r\right)=I$$
6		fveq2	$$⊢r=R\to 0_r=0_R$$
7	6 3	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
8	7	sneqd	$$⊢r=R\to \left\{0_r\right\}=\left\{\underset{\dot{}}{0}\right\}$$
9	8	sneqd	$$⊢r=R\to \left\{\left\{0_r\right\}\right\}=\left\{\left\{\underset{\dot{}}{0}\right\}\right\}$$
10	5 9	difeq12d	$$⊢r=R\to \mathrm{PrmIdeal}\left(r\right)\setminus \left\{\left\{0_r\right\}\right\}=I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}$$
11		fveq2	$$⊢r=R\to \mathrm{RPrime}\left(r\right)=\mathrm{RPrime}\left(R\right)$$
12	11 2	eqtr4di	$$⊢r=R\to \mathrm{RPrime}\left(r\right)=P$$
13	12	ineq2d	$$⊢r=R\to i\cap \mathrm{RPrime}\left(r\right)=i\cap P$$
14	13	neeq1d	$$⊢r=R\to \left(i\cap \mathrm{RPrime}\left(r\right)\ne \varnothing \leftrightarrow i\cap P\ne \varnothing \right)$$
15	10 14	raleqbidv	$$⊢r=R\to \left(\forall i\in \left(\mathrm{PrmIdeal}\left(r\right)\setminus \left\{\left\{0_r\right\}\right\}\right)i\cap \mathrm{RPrime}\left(r\right)\ne \varnothing \leftrightarrow \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)$$
16		df-ufd	$$⊢\mathrm{UFD}=\left\{r\in \mathrm{IDomn}|\forall i\in \left(\mathrm{PrmIdeal}\left(r\right)\setminus \left\{\left\{0_r\right\}\right\}\right)i\cap \mathrm{RPrime}\left(r\right)\ne \varnothing \right\}$$
17	15 16	elrab2	$$⊢R\in \mathrm{UFD}\leftrightarrow \left(R\in \mathrm{IDomn}\wedge \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)$$