Metamath Proof Explorer

Theorem rsprprmprmidl

Description: In a commutative ring, ideals generated by prime elements are prime ideals. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rsprprmprmidl.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
rsprprmprmidl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rsprprmprmidl.p ⊢ ( 𝜑 → 𝑃 ∈ ( RPrime ‘ 𝑅 ) )
Assertion rsprprmprmidl ( 𝜑 → ( 𝐾 ‘ { 𝑃 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rsprprmprmidl.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
2 rsprprmprmidl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
3 rsprprmprmidl.p ⊢ ( 𝜑 → 𝑃 ∈ ( RPrime ‘ 𝑅 ) )
4 2 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( RPrime ‘ 𝑅 ) = ( RPrime ‘ 𝑅 )
7 5 6 2 3 rprmcl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝑅 ) )
8 7 snssd ⊢ ( 𝜑 → { 𝑃 } ⊆ ( Base ‘ 𝑅 ) )
9 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
10 1 5 9 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑃 } ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐾 ‘ { 𝑃 } ) ∈ ( LIdeal ‘ 𝑅 ) )
11 4 8 10 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑃 } ) ∈ ( LIdeal ‘ 𝑅 ) )
12 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
13 5 12 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
14 4 13 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
15 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
16 6 15 2 3 rprmnunit ⊢ ( 𝜑 → ¬ 𝑃 ∈ ( Unit ‘ 𝑅 ) )
17 2 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → 𝑅 ∈ CRing )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
19 15 12 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
20 4 19 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
22 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
23 15 22 dvdsunit ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑃 ∈ ( Unit ‘ 𝑅 ) )
24 17 18 21 23 syl3anc ⊢ ( ( 𝜑 ∧ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → 𝑃 ∈ ( Unit ‘ 𝑅 ) )
25 16 24 mtand ⊢ ( 𝜑 → ¬ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
26 5 1 22 4 7 ellpi ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ↔ 𝑃 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
27 25 26 mtbird ⊢ ( 𝜑 → ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐾 ‘ { 𝑃 } ) )
28 nelne1 ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → ( Base ‘ 𝑅 ) ≠ ( 𝐾 ‘ { 𝑃 } ) )
29 14 27 28 syl2anc ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ≠ ( 𝐾 ‘ { 𝑃 } ) )
30 29 necomd ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑃 } ) ≠ ( Base ‘ 𝑅 ) )
31 5 1 22 4 7 ellpi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ↔ 𝑃 ( ∥r ‘ 𝑅 ) 𝑥 ) )
32 31 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ↔ 𝑃 ( ∥r ‘ 𝑅 ) 𝑥 ) )
33 32 biimpar ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) ∧ 𝑃 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) )
34 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
35 34 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑅 ∈ Ring )
36 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝑅 ) )
37 36 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑃 ∈ ( Base ‘ 𝑅 ) )
38 5 1 22 35 37 ellpi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → ( 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ↔ 𝑃 ( ∥r ‘ 𝑅 ) 𝑦 ) )
39 38 biimpar ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) ∧ 𝑃 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) )
40 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
41 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑅 ∈ CRing )
42 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑃 ∈ ( RPrime ‘ 𝑅 ) )
43 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
44 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
45 5 1 22 34 36 ellpi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ↔ 𝑃 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
46 45 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → 𝑃 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
47 5 6 22 40 41 42 43 44 46 rprmdvds ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → ( 𝑃 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑃 ( ∥r ‘ 𝑅 ) 𝑦 ) )
48 33 39 47 orim12da ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ) )
49 48 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ) ) )
50 49 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ) ) )
51 50 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ) ) )
52 5 40 isprmidlc ⊢ ( 𝑅 ∈ CRing → ( ( 𝐾 ‘ { 𝑃 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( ( 𝐾 ‘ { 𝑃 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝐾 ‘ { 𝑃 } ) ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ) ) ) ) )
53 52 biimpar ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( 𝐾 ‘ { 𝑃 } ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( 𝐾 ‘ { 𝑃 } ) ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐾 ‘ { 𝑃 } ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑃 } ) ∨ 𝑦 ∈ ( 𝐾 ‘ { 𝑃 } ) ) ) ) ) → ( 𝐾 ‘ { 𝑃 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
54 2 11 30 51 53 syl13anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑃 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )