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 ` R )
rsprprmprmidlb.b 
|- B = ( Base ` R )
rsprprmprmidlb.p 
|- P = ( RPrime ` R )
rsprprmprmidlb.k 
|- K = ( RSpan ` R )
rsprprmprmidlb.r 
|- ( ph -> R e. CRing )
rsprprmprmidlb.x 
|- ( ph -> X e. B )
rsprprmprmidlb.1 
|- ( ph -> X =/= .0. )
Assertion rsprprmprmidlb 
|- ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) )

Proof

Step Hyp Ref Expression
1 rsprprmprmidlb.0 
 |-  .0. = ( 0g ` R )
2 rsprprmprmidlb.b 
 |-  B = ( Base ` R )
3 rsprprmprmidlb.p 
 |-  P = ( RPrime ` R )
4 rsprprmprmidlb.k 
 |-  K = ( RSpan ` R )
5 rsprprmprmidlb.r 
 |-  ( ph -> R e. CRing )
6 rsprprmprmidlb.x 
 |-  ( ph -> X e. B )
7 rsprprmprmidlb.1 
 |-  ( ph -> X =/= .0. )
8 5 adantr 
 |-  ( ( ph /\ X e. P ) -> R e. CRing )
9 3 a1i 
 |-  ( ph -> P = ( RPrime ` R ) )
10 9 eleq2d 
 |-  ( ph -> ( X e. P <-> X e. ( RPrime ` R ) ) )
11 10 biimpa 
 |-  ( ( ph /\ X e. P ) -> X e. ( RPrime ` R ) )
12 4 8 11 rsprprmprmidl 
 |-  ( ( ph /\ X e. P ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) )
13 5 adantr 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. CRing )
14 6 adantr 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. B )
15 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
16 eqid 
 |-  ( K ` { X } ) = ( K ` { X } )
17 15 4 16 2 14 13 unitpidl1 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( ( K ` { X } ) = B <-> X e. ( Unit ` R ) ) )
18 17 biimpar 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) = B )
19 13 crngringd 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> R e. Ring )
20 eqid 
 |-  ( .r ` R ) = ( .r ` R )
21 2 20 prmidlnr 
 |-  ( ( R e. Ring /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B )
22 19 21 sylancom 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> ( K ` { X } ) =/= B )
23 22 adantr 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> ( K ` { X } ) =/= B )
24 23 neneqd 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ X e. ( Unit ` R ) ) -> -. ( K ` { X } ) = B )
25 18 24 pm2.65da 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( Unit ` R ) )
26 nelsn 
 |-  ( X =/= .0. -> -. X e. { .0. } )
27 7 26 syl 
 |-  ( ph -> -. X e. { .0. } )
28 27 adantr 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. { .0. } )
29 eqid 
 |-  ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } )
30 nelun 
 |-  ( ( ( Unit ` R ) u. { .0. } ) = ( ( Unit ` R ) u. { .0. } ) -> ( -. X e. ( ( Unit ` R ) u. { .0. } ) <-> ( -. X e. ( Unit ` R ) /\ -. X e. { .0. } ) ) )
31 29 30 ax-mp 
 |-  ( -. X e. ( ( Unit ` R ) u. { .0. } ) <-> ( -. X e. ( Unit ` R ) /\ -. X e. { .0. } ) )
32 25 28 31 sylanbrc 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> -. X e. ( ( Unit ` R ) u. { .0. } ) )
33 14 32 eldifd 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) )
34 eqid 
 |-  ( ||r ` R ) = ( ||r ` R )
35 19 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. Ring )
36 6 ad4antr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> X e. B )
37 2 4 34 35 36 ellpi 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) <-> X ( ||r ` R ) x ) )
38 37 biimpa 
 |-  ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ x e. ( K ` { X } ) ) -> X ( ||r ` R ) x )
39 2 4 34 35 36 ellpi 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( y e. ( K ` { X } ) <-> X ( ||r ` R ) y ) )
40 39 biimpa 
 |-  ( ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) /\ y e. ( K ` { X } ) ) -> X ( ||r ` R ) y )
41 5 ad4antr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> R e. CRing )
42 simp-4r 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( K ` { X } ) e. ( PrmIdeal ` R ) )
43 simpllr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> x e. B )
44 simplr 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> y e. B )
45 19 ad2antrr 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> R e. Ring )
46 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> X e. B )
47 2 4 34 45 46 ellpi 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` R ) y ) e. ( K ` { X } ) <-> X ( ||r ` R ) ( x ( .r ` R ) y ) ) )
48 47 biimpar 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x ( .r ` R ) y ) e. ( K ` { X } ) )
49 2 20 prmidlc 
 |-  ( ( ( R e. CRing /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B /\ ( x ( .r ` R ) y ) e. ( K ` { X } ) ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) )
50 41 42 43 44 48 49 syl23anc 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( x e. ( K ` { X } ) \/ y e. ( K ` { X } ) ) )
51 38 40 50 orim12da 
 |-  ( ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) /\ X ( ||r ` R ) ( x ( .r ` R ) y ) ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) )
52 51 ex 
 |-  ( ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ x e. B ) /\ y e. B ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) )
53 52 anasss 
 |-  ( ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) /\ ( x e. B /\ y e. B ) ) -> ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) )
54 53 ralrimivva 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) )
55 2 15 1 34 20 isrprm 
 |-  ( R e. CRing -> ( X e. ( RPrime ` R ) <-> ( X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) /\ A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) ) )
56 55 biimpar 
 |-  ( ( R e. CRing /\ ( X e. ( B \ ( ( Unit ` R ) u. { .0. } ) ) /\ A. x e. B A. y e. B ( X ( ||r ` R ) ( x ( .r ` R ) y ) -> ( X ( ||r ` R ) x \/ X ( ||r ` R ) y ) ) ) ) -> X e. ( RPrime ` R ) )
57 13 33 54 56 syl12anc 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. ( RPrime ` R ) )
58 57 3 eleqtrrdi 
 |-  ( ( ph /\ ( K ` { X } ) e. ( PrmIdeal ` R ) ) -> X e. P )
59 12 58 impbida 
 |-  ( ph -> ( X e. P <-> ( K ` { X } ) e. ( PrmIdeal ` R ) ) )