Metamath Proof Explorer

Theorem prmidl0

Description: The zero ideal of a commutative ring R is a prime ideal if and only if R is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024)

Ref Expression
Hypothesis prmidl0.1 
|- .0. = ( 0g ` R )
Assertion prmidl0 
|- ( ( R e. CRing /\ { .0. } e. ( PrmIdeal ` R ) ) <-> R e. IDomn )

Proof

Step Hyp Ref Expression
1 prmidl0.1 
 |-  .0. = ( 0g ` R )
2 df-3an 
 |-  ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) <-> ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) )
3 crngring 
 |-  ( R e. CRing -> R e. Ring )
4 3 ad2antrr 
 |-  ( ( ( R e. CRing /\ { .0. } e. ( LIdeal ` R ) ) /\ -. R e. NzRing ) -> R e. Ring )
5 0ringnnzr 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
6 5 biimpar 
 |-  ( ( R e. Ring /\ -. R e. NzRing ) -> ( # ` ( Base ` R ) ) = 1 )
7 4 6 sylancom 
 |-  ( ( ( R e. CRing /\ { .0. } e. ( LIdeal ` R ) ) /\ -. R e. NzRing ) -> ( # ` ( Base ` R ) ) = 1 )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 1 0ring 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> ( Base ` R ) = { .0. } )
10 4 7 9 syl2anc 
 |-  ( ( ( R e. CRing /\ { .0. } e. ( LIdeal ` R ) ) /\ -. R e. NzRing ) -> ( Base ` R ) = { .0. } )
11 10 eqcomd 
 |-  ( ( ( R e. CRing /\ { .0. } e. ( LIdeal ` R ) ) /\ -. R e. NzRing ) -> { .0. } = ( Base ` R ) )
12 11 ex 
 |-  ( ( R e. CRing /\ { .0. } e. ( LIdeal ` R ) ) -> ( -. R e. NzRing -> { .0. } = ( Base ` R ) ) )
13 12 necon1ad 
 |-  ( ( R e. CRing /\ { .0. } e. ( LIdeal ` R ) ) -> ( { .0. } =/= ( Base ` R ) -> R e. NzRing ) )
14 13 impr 
 |-  ( ( R e. CRing /\ ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) ) ) -> R e. NzRing )
15 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
16 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
17 16 1 lidl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
18 15 17 syl 
 |-  ( R e. NzRing -> { .0. } e. ( LIdeal ` R ) )
19 1 fvexi 
 |-  .0. e. _V
20 hashsng 
 |-  ( .0. e. _V -> ( # ` { .0. } ) = 1 )
21 19 20 ax-mp 
 |-  ( # ` { .0. } ) = 1
22 1re 
 |-  1 e. RR
23 21 22 eqeltri 
 |-  ( # ` { .0. } ) e. RR
24 23 a1i 
 |-  ( R e. NzRing -> ( # ` { .0. } ) e. RR )
25 8 isnzr2hash 
 |-  ( R e. NzRing <-> ( R e. Ring /\ 1 < ( # ` ( Base ` R ) ) ) )
26 25 simprbi 
 |-  ( R e. NzRing -> 1 < ( # ` ( Base ` R ) ) )
27 21 26 eqbrtrid 
 |-  ( R e. NzRing -> ( # ` { .0. } ) < ( # ` ( Base ` R ) ) )
28 24 27 ltned 
 |-  ( R e. NzRing -> ( # ` { .0. } ) =/= ( # ` ( Base ` R ) ) )
29 fveq2 
 |-  ( { .0. } = ( Base ` R ) -> ( # ` { .0. } ) = ( # ` ( Base ` R ) ) )
30 29 necon3i 
 |-  ( ( # ` { .0. } ) =/= ( # ` ( Base ` R ) ) -> { .0. } =/= ( Base ` R ) )
31 28 30 syl 
 |-  ( R e. NzRing -> { .0. } =/= ( Base ` R ) )
32 18 31 jca 
 |-  ( R e. NzRing -> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) ) )
33 32 adantl 
 |-  ( ( R e. CRing /\ R e. NzRing ) -> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) ) )
34 14 33 impbida 
 |-  ( R e. CRing -> ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) ) <-> R e. NzRing ) )
35 19 elsn2 
 |-  ( ( x ( .r ` R ) y ) e. { .0. } <-> ( x ( .r ` R ) y ) = .0. )
36 velsn 
 |-  ( x e. { .0. } <-> x = .0. )
37 velsn 
 |-  ( y e. { .0. } <-> y = .0. )
38 36 37 orbi12i 
 |-  ( ( x e. { .0. } \/ y e. { .0. } ) <-> ( x = .0. \/ y = .0. ) )
39 35 38 imbi12i 
 |-  ( ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) <-> ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) )
40 39 2ralbii 
 |-  ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) <-> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) )
41 40 a1i 
 |-  ( R e. CRing -> ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) <-> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
42 34 41 anbi12d 
 |-  ( R e. CRing -> ( ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) <-> ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
43 2 42 syl5bb 
 |-  ( R e. CRing -> ( ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) <-> ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
44 43 pm5.32i 
 |-  ( ( R e. CRing /\ ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) ) <-> ( R e. CRing /\ ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
45 eqid 
 |-  ( .r ` R ) = ( .r ` R )
46 8 45 isprmidlc 
 |-  ( R e. CRing -> ( { .0. } e. ( PrmIdeal ` R ) <-> ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) ) )
47 46 pm5.32i 
 |-  ( ( R e. CRing /\ { .0. } e. ( PrmIdeal ` R ) ) <-> ( R e. CRing /\ ( { .0. } e. ( LIdeal ` R ) /\ { .0. } =/= ( Base ` R ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) e. { .0. } -> ( x e. { .0. } \/ y e. { .0. } ) ) ) ) )
48 df-idom 
 |-  IDomn = ( CRing i^i Domn )
49 48 eleq2i 
 |-  ( R e. IDomn <-> R e. ( CRing i^i Domn ) )
50 elin 
 |-  ( R e. ( CRing i^i Domn ) <-> ( R e. CRing /\ R e. Domn ) )
51 8 45 1 isdomn 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
52 51 anbi2i 
 |-  ( ( R e. CRing /\ R e. Domn ) <-> ( R e. CRing /\ ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
53 49 50 52 3bitri 
 |-  ( R e. IDomn <-> ( R e. CRing /\ ( R e. NzRing /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
54 44 47 53 3bitr4i 
 |-  ( ( R e. CRing /\ { .0. } e. ( PrmIdeal ` R ) ) <-> R e. IDomn )