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 ˙ = 0 R
Assertion prmidl0 Could not format assertion : No typesetting found for |- ( ( R e. CRing /\ { .0. } e. ( PrmIdeal ` R ) ) <-> R e. IDomn ) with typecode |-

Proof

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