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 bilani ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ ( Irred ‘ 𝑅 ) )
39 eqid ⊢ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } )
40 7 snssd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → { 𝑝 } ⊆ ( Base ‘ 𝑅 ) )
41 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
42 27 5 41 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑝 } ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( LIdeal ‘ 𝑅 ) )
43 15 40 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( LIdeal ‘ 𝑅 ) )
44 5 27 17 39 4 7 19 43 mxidlirred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑝 ∈ ( Irred ‘ 𝑅 ) ) )
45 38 44 mpbird ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) )
46 45 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) )
47 eqid ⊢ ( LSSum ‘ ( mulGrp ‘ 𝑅 ) ) = ( LSSum ‘ ( mulGrp ‘ 𝑅 ) )
48 47 mxidlprm ⊢ ( ( 𝑅 ∈ CRing ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
49 36 46 48 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
50 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
51 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
52 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
53 5 27 28 29 30 ellpi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ↔ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
54 52 53 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) )
55 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
56 5 55 prmidlc ⊢ ( ( ( 𝑅 ∈ CRing ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) ) → ( 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∨ 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) )
57 36 49 50 51 54 56 syl23anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ∨ 𝑦 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑝 } ) ) )
58 32 34 57 orim12da ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) )
59 58 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
60 59 anasss ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
61 60 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) )
62 5 8 17 28 55 isrprm ⊢ ( 𝑅 ∈ PID → ( 𝑝 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑝 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) )
63 62 biimpar ⊢ ( ( 𝑅 ∈ PID ∧ ( 𝑝 ∈ ( ( Base ‘ 𝑅 ) ∖ ( ( Unit ‘ 𝑅 ) ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑝 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑝 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑝 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) → 𝑝 ∈ ( RPrime ‘ 𝑅 ) )
64 4 26 61 63 syl12anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ ( RPrime ‘ 𝑅 ) )
65 64 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐼 ) → 𝑝 ∈ 𝑃 )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
67 13 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑅 ∈ IDomn )
68 1 2 66 67 rprmirred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝑝 ∈ 𝐼 )
69 65 68 impbida ⊢ ( 𝜑 → ( 𝑝 ∈ 𝐼 ↔ 𝑝 ∈ 𝑃 ) )
70 69 eqrdv ⊢ ( 𝜑 → 𝐼 = 𝑃 )