Theorem isufd

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

	Ref	Expression
Hypotheses	isufd.i	⊢ 𝐼 = ( PrmIdeal ‘ 𝑅 )
	isufd.3	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
	isufd.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) )

Proof

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