Metamath Proof Explorer

Theorem rsprprmprmidlb

Description: In an integral domain, an ideal generated by a single element is a prime iff that element is prime. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rsprprmprmidlb.0 ⊢ 0 = ( 0g ‘ 𝑅 )
rsprprmprmidlb.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rsprprmprmidlb.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rsprprmprmidlb.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
rsprprmprmidlb.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
rsprprmprmidlb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rsprprmprmidlb.1 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion rsprprmprmidlb ( 𝜑 → ( 𝑋 ∈ 𝑃 ↔ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 rsprprmprmidlb.0 ⊢ 0 = ( 0g ‘ 𝑅 )
2 rsprprmprmidlb.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 rsprprmprmidlb.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
4 rsprprmprmidlb.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
5 rsprprmprmidlb.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
6 rsprprmprmidlb.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 rsprprmprmidlb.1 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
8 5 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑃 ) → 𝑅 ∈ CRing )
10 3 a1i ⊢ ( 𝜑 → 𝑃 = ( RPrime ‘ 𝑅 ) )
11 10 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑃 ↔ 𝑋 ∈ ( RPrime ‘ 𝑅 ) ) )
12 11 biimpa ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ∈ ( RPrime ‘ 𝑅 ) )
13 4 9 12 rsprprmprmidl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑃 ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
14 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑅 ∈ IDomn )
15 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑋 ∈ 𝐵 )
16 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
17 eqid ⊢ ( 𝐾 ‘ { 𝑋 } ) = ( 𝐾 ‘ { 𝑋 } )
18 16 4 17 2 15 14 unitpidl1 ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( ( 𝐾 ‘ { 𝑋 } ) = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
19 18 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐾 ‘ { 𝑋 } ) = 𝐵 )
20 14 idomringd ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
21 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
22 2 21 prmidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝐾 ‘ { 𝑋 } ) ≠ 𝐵 )
23 20 22 sylancom ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ( 𝐾 ‘ { 𝑋 } ) ≠ 𝐵 )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐾 ‘ { 𝑋 } ) ≠ 𝐵 )
25 24 neneqd ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) → ¬ ( 𝐾 ‘ { 𝑋 } ) = 𝐵 )
26 19 25 pm2.65da ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
27 nelsn ⊢ ( 𝑋 ≠ 0 → ¬ 𝑋 ∈ { 0 } )
28 7 27 syl ⊢ ( 𝜑 → ¬ 𝑋 ∈ { 0 } )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ¬ 𝑋 ∈ { 0 } )
30 eqid ⊢ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) = ( ( Unit ‘ 𝑅 ) ∪ { 0 } )
31 nelun ⊢ ( ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) = ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) → ( ¬ 𝑋 ∈ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ↔ ( ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) ∧ ¬ 𝑋 ∈ { 0 } ) ) )
32 30 31 ax-mp ⊢ ( ¬ 𝑋 ∈ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ↔ ( ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) ∧ ¬ 𝑋 ∈ { 0 } ) )
33 26 29 32 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ¬ 𝑋 ∈ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) )
34 15 33 eldifd ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑋 ∈ ( 𝐵 ∖ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) )
35 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
36 20 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑅 ∈ Ring )
37 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑋 ∈ 𝐵 )
38 2 4 35 36 37 ellpi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ) )
39 38 biimpa ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) ∧ 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 )
40 2 4 35 36 37 ellpi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑦 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) )
41 40 biimpa ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) ∧ 𝑦 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 )
42 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑅 ∈ CRing )
43 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
44 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑥 ∈ 𝐵 )
45 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑦 ∈ 𝐵 )
46 20 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑅 ∈ Ring )
47 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
48 2 4 35 46 47 ellpi ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
49 48 biimpar ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑋 } ) )
50 2 21 prmidlc ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑋 } ) ) ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑋 } ) ) )
51 42 43 44 45 49 50 syl23anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑋 } ) ) )
52 39 41 51 orim12da ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) )
53 52 ex ⊢ ( ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
54 53 anasss ⊢ ( ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
55 54 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
56 2 16 1 35 21 isrprm ⊢ ( 𝑅 ∈ IDomn → ( 𝑋 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑋 ∈ ( 𝐵 ∖ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) )
57 56 biimpar ⊢ ( ( 𝑅 ∈ IDomn ∧ ( 𝑋 ∈ ( 𝐵 ∖ ( ( Unit ‘ 𝑅 ) ∪ { 0 } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑋 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) → 𝑋 ∈ ( RPrime ‘ 𝑅 ) )
58 14 34 55 57 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑋 ∈ ( RPrime ‘ 𝑅 ) )
59 58 3 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑋 ∈ 𝑃 )
60 13 59 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑃 ↔ ( 𝐾 ‘ { 𝑋 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) )