Theorem isufd

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

	Ref	Expression
Hypotheses	isufd.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	isufd.i	⊢ 𝐼 = ( PrmIdeal ‘ 𝑅 )
	isufd.3	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
Assertion	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ CRing ∧ ( 𝐴 ≠ ∅ ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		isufd.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		isufd.i	⊢ 𝐼 = ( PrmIdeal ‘ 𝑅 )
3		isufd.3	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( AbsVal ‘ 𝑟 ) = ( AbsVal ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( AbsVal ‘ 𝑟 ) = 𝐴 )
6	5	neeq1d	⊢ ( 𝑟 = 𝑅 → ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
7		fveq2	⊢ ( 𝑟 = 𝑅 → ( PrmIdeal ‘ 𝑟 ) = ( PrmIdeal ‘ 𝑅 ) )
8	7 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( PrmIdeal ‘ 𝑟 ) = 𝐼 )
9		fveq2	⊢ ( 𝑟 = 𝑅 → ( RPrime ‘ 𝑟 ) = ( RPrime ‘ 𝑅 ) )
10	9 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( RPrime ‘ 𝑟 ) = 𝑃 )
11	10	ineq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) = ( 𝑖 ∩ 𝑃 ) )
12	11	neeq1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ↔ ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) )
13	8 12	raleqbidv	⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) )
14	6 13	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ) ↔ ( 𝐴 ≠ ∅ ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )
15		df-ufd	⊢ UFD = { 𝑟 ∈ CRing ∣ ( ( AbsVal ‘ 𝑟 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( PrmIdeal ‘ 𝑟 ) ( 𝑖 ∩ ( RPrime ‘ 𝑟 ) ) ≠ ∅ ) }
16	14 15	elrab2	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ CRing ∧ ( 𝐴 ≠ ∅ ∧ ∀ 𝑖 ∈ 𝐼 ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )