Metamath Proof Explorer

Theorem rsprprmprmidlb

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