Theorem isufd2

Description: Alternate definition of unique factorization domains, using integral domains, for nonzero rings. (Contributed by Thierry Arnoux, 18-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isufd2.1	⊢ 𝐼 = ( PrmIdeal ‘ 𝑅 )
2		isufd2.2	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
3		isufd2.3	⊢ 0 = ( 0g ‘ 𝑅 )
4		eqid	⊢ ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑅 )
5	4 1 2 3	isufd	⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ CRing ∧ ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )
6		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
7	4	abvn0b	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( AbsVal ‘ 𝑅 ) ≠ ∅ ) )
8	7	baib	⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ Domn ↔ ( AbsVal ‘ 𝑅 ) ≠ ∅ ) )
9	8	anbi2d	⊢ ( 𝑅 ∈ NzRing → ( ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) ↔ ( 𝑅 ∈ CRing ∧ ( AbsVal ‘ 𝑅 ) ≠ ∅ ) ) )
10	6 9	bitrid	⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ ( AbsVal ‘ 𝑅 ) ≠ ∅ ) ) )
11	10	anbi1d	⊢ ( 𝑅 ∈ NzRing → ( ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ↔ ( ( 𝑅 ∈ CRing ∧ ( AbsVal ‘ 𝑅 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )
12		anass	⊢ ( ( ( 𝑅 ∈ CRing ∧ ( AbsVal ‘ 𝑅 ) ≠ ∅ ) ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ↔ ( 𝑅 ∈ CRing ∧ ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )
13	11 12	bitr2di	⊢ ( 𝑅 ∈ NzRing → ( ( 𝑅 ∈ CRing ∧ ( ( AbsVal ‘ 𝑅 ) ≠ ∅ ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )
14	5 13	bitrid	⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( 𝐼 ∖ { { 0 } } ) ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) ) )