Metamath Proof Explorer

Theorem rprmirredb

Description: In a principal ideal domain, the converse of rprmirred holds, i.e. irreducible elements are prime. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmirredb.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmirredb.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
rprmirredb.r ⊢ ( 𝜑 → 𝑅 ∈ PID )
Assertion rprmirredb ( 𝜑 → 𝐼 = 𝑃 )

Proof

Step Hyp Ref Expression
1 rprmirredb.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
2 rprmirredb.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
3 rprmirredb.r ⊢ ( 𝜑 → 𝑅 ∈ PID )
4 3 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑅 ∈ PID )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 2 5 irredcl ⊢ ( 𝑝 ∈ 𝐼 → 𝑝 ∈ ( Base ‘ 𝑅 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ ( Base ‘ 𝑅 ) )
8 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
9 2 8 irrednu ⊢ ( 𝑝 ∈ 𝐼 → ¬ 𝑝 ∈ ( Unit ‘ 𝑅 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ¬ 𝑝 ∈ ( Unit ‘ 𝑅 ) )
11 df-pid ⊢ PID = ( IDomn ∩ LPIR )
12 3 11 eleqtrdi ⊢ ( 𝜑 → 𝑅 ∈ ( IDomn ∩ LPIR ) )
13 12 elin1d ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
14 13 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑅 ∈ Ring )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ 𝐼 )
17 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18 2 17 irredn0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ≠ ( 0g ‘ 𝑅 ) )
19 15 16 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ≠ ( 0g ‘ 𝑅 ) )
20 nelsn ⊢ ( 𝑝 ≠ ( 0g ‘ 𝑅 ) → ¬ 𝑝 ∈ { ( 0g ‘ 𝑅 ) } )
21 19 20 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ¬ 𝑝 ∈ { ( 0g ‘ 𝑅 ) } )
22 eqid ⊢ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) = ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } )
23 nelun ⊢ ( ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) = ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) → ( ¬ 𝑝 ∈ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ↔ ( ¬ 𝑝 ∈ ( Unit ‘ 𝑅 ) ∧ ¬ 𝑝 ∈ { ( 0g ‘ 𝑅 ) } ) ) )
24 22 23 ax-mp ⊢ ( ¬ 𝑝 ∈ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ↔ ( ¬ 𝑝 ∈ ( Unit ‘ 𝑅 ) ∧ ¬ 𝑝 ∈ { ( 0g ‘ 𝑅 ) } ) )
25 10 21 24 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ¬ 𝑝 ∈ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) )
26 7 25 eldifd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) )
27 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
28 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
29 15 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑅 ∈ Ring )
30 7 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑝 ∈ ( Base ‘ 𝑅 ) )
31 5 27 28 29 30 ellpi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ↔ 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ) )
32 31 biimpa ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) ∧ 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) → 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 )
33 5 27 28 29 30 ellpi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ↔ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) )
34 33 biimpa ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) ∧ 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) → 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 )
35 13 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
36 35 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑅 ∈ CRing )
37 2 eleq2i ⊢ ( 𝑝 ∈ 𝐼 ↔ 𝑝 ∈ ( Irred ‘ 𝑅 ) )
38 37 biimpi ⊢ ( 𝑝 ∈ 𝐼 → 𝑝 ∈ ( Irred ‘ 𝑅 ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ ( Irred ‘ 𝑅 ) )
40 eqid ⊢ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } )
41 7 snssd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → { 𝑝 } ⊆ ( Base ‘ 𝑅 ) )
42 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
43 27 5 42 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑝 } ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( LIdeal ‘ 𝑅 ) )
44 15 41 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( LIdeal ‘ 𝑅 ) )
45 5 27 17 40 4 7 19 44 mxidlirred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑝 ∈ ( Irred ‘ 𝑅 ) ) )
46 39 45 mpbird ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) )
47 46 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) )
48 eqid ⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
49 48 mxidlprm ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
50 36 47 49 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
51 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
52 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
53 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
54 5 27 28 29 30 ellpi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ↔ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
55 53 54 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) )
56 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
57 5 56 prmidlc ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) ) → ( 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∨ 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) )
58 36 50 51 52 55 57 syl23anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∨ 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) )
59 32 34 58 orim12da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) )
60 59 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
61 60 anasss ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
62 61 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
63 5 8 17 28 56 isrprm ⊢ ( 𝑅 ∈ PID → ( 𝑝 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑝 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) )
64 63 biimpar ⊢ ( ( 𝑅 ∈ PID ∧ ( 𝑝 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) → 𝑝 ∈ ( RPrime ‘ 𝑅 ) )
65 4 26 62 64 syl12anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ ( RPrime ‘ 𝑅 ) )
66 65 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ 𝑃 )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
68 13 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑅 ∈ IDomn )
69 1 2 67 68 rprmirred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝐼 )
70 66 69 impbida ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐼 ↔ 𝑝 ∈ 𝑃 ) )
71 70 eqrdv ⊢ ( 𝜑 → 𝐼 = 𝑃 )