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 
|- K = ( RSpan ` R )
rsprprmprmidl.r 
|- ( ph -> R e. CRing )
rsprprmprmidl.p 
|- ( ph -> P e. ( RPrime ` R ) )
Assertion rsprprmprmidl 
|- ( ph -> ( K ` { P } ) e. ( PrmIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 rsprprmprmidl.k 
 |-  K = ( RSpan ` R )
2 rsprprmprmidl.r 
 |-  ( ph -> R e. CRing )
3 rsprprmprmidl.p 
 |-  ( ph -> P e. ( RPrime ` R ) )
4 2 crngringd 
 |-  ( ph -> R e. Ring )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( RPrime ` R ) = ( RPrime ` R )
7 5 6 2 3 rprmcl 
 |-  ( ph -> P e. ( Base ` R ) )
8 7 snssd 
 |-  ( ph -> { P } C_ ( Base ` R ) )
9 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
10 1 5 9 rspcl 
 |-  ( ( R e. Ring /\ { P } C_ ( Base ` R ) ) -> ( K ` { P } ) e. ( LIdeal ` R ) )
11 4 8 10 syl2anc 
 |-  ( ph -> ( K ` { P } ) e. ( LIdeal ` R ) )
12 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
13 5 12 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
14 4 13 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
15 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
16 6 15 2 3 rprmnunit 
 |-  ( ph -> -. P e. ( Unit ` R ) )
17 2 adantr 
 |-  ( ( ph /\ P ( ||r ` R ) ( 1r ` R ) ) -> R e. CRing )
18 simpr 
 |-  ( ( ph /\ P ( ||r ` R ) ( 1r ` R ) ) -> P ( ||r ` R ) ( 1r ` R ) )
19 15 12 1unit 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
20 4 19 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Unit ` R ) )
21 20 adantr 
 |-  ( ( ph /\ P ( ||r ` R ) ( 1r ` R ) ) -> ( 1r ` R ) e. ( Unit ` R ) )
22 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
23 15 22 dvdsunit 
 |-  ( ( R e. CRing /\ P ( ||r ` R ) ( 1r ` R ) /\ ( 1r ` R ) e. ( Unit ` R ) ) -> P e. ( Unit ` R ) )
24 17 18 21 23 syl3anc 
 |-  ( ( ph /\ P ( ||r ` R ) ( 1r ` R ) ) -> P e. ( Unit ` R ) )
25 16 24 mtand 
 |-  ( ph -> -. P ( ||r ` R ) ( 1r ` R ) )
26 5 1 22 4 7 ellpi 
 |-  ( ph -> ( ( 1r ` R ) e. ( K ` { P } ) <-> P ( ||r ` R ) ( 1r ` R ) ) )
27 25 26 mtbird 
 |-  ( ph -> -. ( 1r ` R ) e. ( K ` { P } ) )
28 nelne1 
 |-  ( ( ( 1r ` R ) e. ( Base ` R ) /\ -. ( 1r ` R ) e. ( K ` { P } ) ) -> ( Base ` R ) =/= ( K ` { P } ) )
29 14 27 28 syl2anc 
 |-  ( ph -> ( Base ` R ) =/= ( K ` { P } ) )
30 29 necomd 
 |-  ( ph -> ( K ` { P } ) =/= ( Base ` R ) )
31 5 1 22 4 7 ellpi 
 |-  ( ph -> ( x e. ( K ` { P } ) <-> P ( ||r ` R ) x ) )
32 31 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> ( x e. ( K ` { P } ) <-> P ( ||r ` R ) x ) )
33 32 biimpar 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) /\ P ( ||r ` R ) x ) -> x e. ( K ` { P } ) )
34 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> R e. Ring )
35 34 adantr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> R e. Ring )
36 7 ad2antrr 
 |-  ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> P e. ( Base ` R ) )
37 36 adantr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> P e. ( Base ` R ) )
38 5 1 22 35 37 ellpi 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> ( y e. ( K ` { P } ) <-> P ( ||r ` R ) y ) )
39 38 biimpar 
 |-  ( ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) /\ P ( ||r ` R ) y ) -> y e. ( K ` { P } ) )
40 eqid 
 |-  ( .r ` R ) = ( .r ` R )
41 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> R e. CRing )
42 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> P e. ( RPrime ` R ) )
43 simpllr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> x e. ( Base ` R ) )
44 simplr 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> y e. ( Base ` R ) )
45 5 1 22 34 36 ellpi 
 |-  ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) e. ( K ` { P } ) <-> P ( ||r ` R ) ( x ( .r ` R ) y ) ) )
46 45 biimpa 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> P ( ||r ` R ) ( x ( .r ` R ) y ) )
47 5 6 22 40 41 42 43 44 46 rprmdvds 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> ( P ( ||r ` R ) x \/ P ( ||r ` R ) y ) )
48 33 39 47 orim12da 
 |-  ( ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) /\ ( x ( .r ` R ) y ) e. ( K ` { P } ) ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) )
49 48 ex 
 |-  ( ( ( ph /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) )
50 49 anasss 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) )
51 50 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) )
52 5 40 isprmidlc 
 |-  ( R e. CRing -> ( ( K ` { P } ) e. ( PrmIdeal ` R ) <-> ( ( K ` { P } ) e. ( LIdeal ` R ) /\ ( K ` { P } ) =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) ) ) )
53 52 biimpar 
 |-  ( ( R e. CRing /\ ( ( K ` { P } ) e. ( LIdeal ` R ) /\ ( K ` { P } ) =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. ( K ` { P } ) -> ( x e. ( K ` { P } ) \/ y e. ( K ` { P } ) ) ) ) ) -> ( K ` { P } ) e. ( PrmIdeal ` R ) )
54 2 11 30 51 53 syl13anc 
 |-  ( ph -> ( K ` { P } ) e. ( PrmIdeal ` R ) )