Metamath Proof Explorer

Theorem pidufd

Description: Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypothesis pidufd.1 ⊢ ( 𝜑 → 𝑅 ∈ PID )
Assertion pidufd ( 𝜑 → 𝑅 ∈ UFD )

Proof

Step Hyp Ref Expression
1 pidufd.1 ⊢ ( 𝜑 → 𝑅 ∈ PID )
2 df-pid ⊢ PID = ( IDomn ∩ LPIR )
3 1 2 eleqtrdi ⊢ ( 𝜑 → 𝑅 ∈ ( IDomn ∩ LPIR ) )
4 3 elin1d ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 4 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑅 ∈ Ring )
7 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
10 8 9 rspsnid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
11 6 7 10 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
12 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
13 11 12 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑖 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) )
15 14 eldifad ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
16 15 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
17 12 16 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 eqid ⊢ ( RPrime ‘ 𝑅 ) = ( RPrime ‘ 𝑅 )
20 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑅 ∈ IDomn )
21 20 idomcringd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑅 ∈ CRing )
22 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
23 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑥 = ( 0g ‘ 𝑅 ) )
24 23 sneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → { 𝑥 } = { ( 0g ‘ 𝑅 ) } )
25 24 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) )
26 9 18 rsp0 ⊢ ( 𝑅 ∈ Ring → ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) = { ( 0g ‘ 𝑅 ) } )
27 5 26 syl ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) = { ( 0g ‘ 𝑅 ) } )
28 27 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) = { ( 0g ‘ 𝑅 ) } )
29 22 25 28 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑖 = { ( 0g ‘ 𝑅 ) } )
30 eldifsni ⊢ ( 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) → 𝑖 ≠ { ( 0g ‘ 𝑅 ) } )
31 30 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑖 ≠ { ( 0g ‘ 𝑅 ) } )
32 31 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → ¬ 𝑖 = { ( 0g ‘ 𝑅 ) } )
33 29 32 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ¬ 𝑥 = ( 0g ‘ 𝑅 ) )
34 33 neqned ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ≠ ( 0g ‘ 𝑅 ) )
35 18 8 19 9 21 7 34 rsprprmprmidlb ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ( 𝑥 ∈ ( RPrime ‘ 𝑅 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) )
36 17 35 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( RPrime ‘ 𝑅 ) )
37 13 36 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) )
38 37 ne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
39 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
40 3 elin2d ⊢ ( 𝜑 → 𝑅 ∈ LPIR )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑅 ∈ LPIR )
42 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑅 ∈ Ring )
43 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
44 42 15 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
45 8 39 9 41 44 lpirlidllpi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
46 38 45 r19.29a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
47 46 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
48 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
49 48 19 18 isufd ⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) )
50 4 47 49 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ UFD )