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 ‘ 𝑅 )
	isufd.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ CRing ∧ ( 𝐴 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )

Proof

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