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)$$
Assertion	isufd	Could not format assertion : No typesetting found for |- ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. I ( 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		fveq2	$$⊢r=R\to \mathrm{AbsVal}\left(r\right)=\mathrm{AbsVal}\left(R\right)$$
5	4 1	eqtr4di	$$⊢r=R\to \mathrm{AbsVal}\left(r\right)=A$$
6	5	neeq1d	$$⊢r=R\to \left(\mathrm{AbsVal}\left(r\right)\ne \varnothing \leftrightarrow A\ne \varnothing \right)$$
7		fveq2	Could not format ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ) : No typesetting found for |- ( r = R -> ( PrmIdeal ` r ) = ( PrmIdeal ` R ) ) with typecode |-
8	7 2	eqtr4di	Could not format ( r = R -> ( PrmIdeal ` r ) = I ) : No typesetting found for |- ( r = R -> ( PrmIdeal ` r ) = I ) with typecode |-
9		fveq2	$$⊢r=R\to \mathrm{RPrime}\left(r\right)=\mathrm{RPrime}\left(R\right)$$
10	9 3	eqtr4di	$$⊢r=R\to \mathrm{RPrime}\left(r\right)=P$$
11	10	ineq2d	$$⊢r=R\to i\cap \mathrm{RPrime}\left(r\right)=i\cap P$$
12	11	neeq1d	$$⊢r=R\to \left(i\cap \mathrm{RPrime}\left(r\right)\ne \varnothing \leftrightarrow i\cap P\ne \varnothing \right)$$
13	8 12	raleqbidv	Could not format ( r = R -> ( A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. I ( i i^i P ) =/= (/) ) ) : No typesetting found for |- ( r = R -> ( A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) <-> A. i e. I ( i i^i P ) =/= (/) ) ) with typecode |-
14	6 13	anbi12d	Could not format ( r = R -> ( ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) <-> ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) ) : No typesetting found for |- ( r = R -> ( ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) <-> ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) ) with typecode |-
15		df-ufd	Could not format UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } : No typesetting found for |- UFD = { r e. CRing | ( ( AbsVal ` r ) =/= (/) /\ A. i e. ( PrmIdeal ` r ) ( i i^i ( RPrime ` r ) ) =/= (/) ) } with typecode |-
16	14 15	elrab2	Could not format ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) ) : No typesetting found for |- ( R e. UFD <-> ( R e. CRing /\ ( A =/= (/) /\ A. i e. I ( i i^i P ) =/= (/) ) ) ) with typecode |-