Theorem isufd

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

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

Proof

Step	Hyp	Ref	Expression
1		isufd.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		isufd.i	Could not format I = ( PrmIdeal ` R ) : No typesetting found for |- I = ( PrmIdeal ` R ) with typecode |-
3		isufd.3	$$⊢P=\mathrm{RPrime}\left(R\right)$$
4		isufd.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		fveq2	$$⊢r=R\to \mathrm{AbsVal}\left(r\right)=\mathrm{AbsVal}\left(R\right)$$
6	5 1	eqtr4di	$$⊢r=R\to \mathrm{AbsVal}\left(r\right)=A$$
7	6	neeq1d	$$⊢r=R\to \left(\mathrm{AbsVal}\left(r\right)\ne \varnothing \leftrightarrow A\ne \varnothing \right)$$
8		fveq2	Could not format ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ) : No typesetting found for |- ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ) with typecode |-
9	8 2	eqtr4di	Could not format ( r = R -> ( PrmIdeal ` r ) = I ) : No typesetting found for |- ( r = R -> ( PrmIdeal ` r ) = I ) with typecode |-
10		fveq2	$$⊢r=R\to 0_r=0_R$$
11	10 4	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
12	11	sneqd	$$⊢r=R\to \left\{0_r\right\}=\left\{\underset{\dot{}}{0}\right\}$$
13	12	sneqd	$$⊢r=R\to \left\{\left\{0_r\right\}\right\}=\left\{\left\{\underset{\dot{}}{0}\right\}\right\}$$
14	9 13	difeq12d	Could not format ( r = R -> ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) = ( I \ { { .0. } } ) ) : No typesetting found for |- ( r = R -> ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) = ( I \ { { .0. } } ) ) with typecode |-
15		fveq2	$$⊢r=R\to \mathrm{RPrime}\left(r\right)=\mathrm{RPrime}\left(R\right)$$
16	15 3	eqtr4di	$$⊢r=R\to \mathrm{RPrime}\left(r\right)=P$$
17	16	ineq2d	$$⊢r=R\to i\cap \mathrm{RPrime}\left(r\right)=i\cap P$$
18	17	neeq1d	$$⊢r=R\to \left(i\cap \mathrm{RPrime}\left(r\right)\ne \varnothing \leftrightarrow i\cap P\ne \varnothing \right)$$
19	14 18	raleqbidv	Could not format ( r = R -> ( A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) : No typesetting found for |- ( r = R -> ( A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) with typecode |-
20	7 19	anbi12d	Could not format ( r = R -> ( ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) <-> ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) : No typesetting found for |- ( r = R -> ( ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) <-> ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) with typecode |-
21		df-ufd	Could not format UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } : No typesetting found for |- UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( ( PrmIdeal ` r ) \ { { ( 0g ` r ) } } ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } with typecode |-
22	20 21	elrab2	Could not format ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) : No typesetting found for |- ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. ( I \ { { .0. } } ) ( i i^i P ) =/= (/) ) ) ) with typecode |-