Theorem isufd2

Description: Alternate definition of unique factorization domains, using integral domains, for nonzero rings. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	isufd2.1	No typesetting found for |- I = ( PrmIdeal ` R ) with typecode |-
	isufd2.2	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	isufd2.3	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	isufd2	Could not format assertion : No typesetting found for |- ( R e. NzRing -> ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		isufd2.1	Could not format I = ( PrmIdeal ` R ) : No typesetting found for |- I = ( PrmIdeal ` R ) with typecode |-
2		isufd2.2	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		isufd2.3	$$⊢\underset{\dot{}}{0}=0_R$$
4		eqid	$$⊢\mathrm{AbsVal}\left(R\right)=\mathrm{AbsVal}\left(R\right)$$
5	4 1 2 3	isufd	Could not format ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) : No typesetting found for |- ( R e. UFD <-> ( R e. CRing /\ ( ( AbsVal ` R ) =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) with typecode |-
6		isidom	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
7	4	abvn0b	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \mathrm{AbsVal}\left(R\right)\ne \varnothing \right)$$
8	7	baib	$$⊢R\in \mathrm{NzRing}\to \left(R\in \mathrm{Domn}\leftrightarrow \mathrm{AbsVal}\left(R\right)\ne \varnothing \right)$$
9	8	anbi2d	$$⊢R\in \mathrm{NzRing}\to \left(\left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge \mathrm{AbsVal}\left(R\right)\ne \varnothing \right)\right)$$
10	6 9	bitrid	$$⊢R\in \mathrm{NzRing}\to \left(R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge \mathrm{AbsVal}\left(R\right)\ne \varnothing \right)\right)$$
11	10	anbi1d	$$⊢R\in \mathrm{NzRing}\to \left(\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)\leftrightarrow \left(\left(R\in \mathrm{CRing}\wedge \mathrm{AbsVal}\left(R\right)\ne \varnothing \right)\wedge \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)\right)$$
12		anass	$$⊢\left(\left(R\in \mathrm{CRing}\wedge \mathrm{AbsVal}\left(R\right)\ne \varnothing \right)\wedge \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)\leftrightarrow \left(R\in \mathrm{CRing}\wedge \left(\mathrm{AbsVal}\left(R\right)\ne \varnothing \wedge \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)\right)$$
13	11 12	bitr2di	$$⊢R\in \mathrm{NzRing}\to \left(\left(R\in \mathrm{CRing}\wedge \left(\mathrm{AbsVal}\left(R\right)\ne \varnothing \wedge \forall i\in \left(I\setminus \left\{\left\{\underset{\dot{}}{0}\right\}\right\}\right)i\cap P\ne \varnothing \right)\right)\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)\right)$$
14	5 13	bitrid	Could not format ( R e. NzRing -> ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) : No typesetting found for |- ( R e. NzRing -> ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) with typecode |-