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˙=0R
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˙=0R
2 df-3an 0˙LIdealR0˙BaseRxBaseRyBaseRxRy0˙x0˙y0˙0˙LIdealR0˙BaseRxBaseRyBaseRxRy0˙x0˙y0˙
3 crngring RCRingRRing
4 3 ad2antrr RCRing0˙LIdealR¬RNzRingRRing
5 0ringnnzr RRingBaseR=1¬RNzRing
6 5 biimpar RRing¬RNzRingBaseR=1
7 4 6 sylancom RCRing0˙LIdealR¬RNzRingBaseR=1
8 eqid BaseR=BaseR
9 8 1 0ring RRingBaseR=1BaseR=0˙
10 4 7 9 syl2anc RCRing0˙LIdealR¬RNzRingBaseR=0˙
11 10 eqcomd RCRing0˙LIdealR¬RNzRing0˙=BaseR
12 11 ex RCRing0˙LIdealR¬RNzRing0˙=BaseR
13 12 necon1ad RCRing0˙LIdealR0˙BaseRRNzRing
14 13 impr RCRing0˙LIdealR0˙BaseRRNzRing
15 nzrring RNzRingRRing
16 eqid LIdealR=LIdealR
17 16 1 lidl0 RRing0˙LIdealR
18 15 17 syl RNzRing0˙LIdealR
19 1 fvexi 0˙V
20 hashsng 0˙V0˙=1
21 19 20 ax-mp 0˙=1
22 1re 1
23 21 22 eqeltri 0˙
24 23 a1i RNzRing0˙
25 8 isnzr2hash RNzRingRRing1<BaseR
26 25 simprbi RNzRing1<BaseR
27 21 26 eqbrtrid RNzRing0˙<BaseR
28 24 27 ltned RNzRing0˙BaseR
29 fveq2 0˙=BaseR0˙=BaseR
30 29 necon3i 0˙BaseR0˙BaseR
31 28 30 syl RNzRing0˙BaseR
32 18 31 jca RNzRing0˙LIdealR0˙BaseR
33 32 adantl RCRingRNzRing0˙LIdealR0˙BaseR
34 14 33 impbida RCRing0˙LIdealR0˙BaseRRNzRing
35 19 elsn2 xRy0˙xRy=0˙
36 velsn x0˙x=0˙
37 velsn y0˙y=0˙
38 36 37 orbi12i x0˙y0˙x=0˙y=0˙
39 35 38 imbi12i xRy0˙x0˙y0˙xRy=0˙x=0˙y=0˙
40 39 2ralbii xBaseRyBaseRxRy0˙x0˙y0˙xBaseRyBaseRxRy=0˙x=0˙y=0˙
41 40 a1i RCRingxBaseRyBaseRxRy0˙x0˙y0˙xBaseRyBaseRxRy=0˙x=0˙y=0˙
42 34 41 anbi12d RCRing0˙LIdealR0˙BaseRxBaseRyBaseRxRy0˙x0˙y0˙RNzRingxBaseRyBaseRxRy=0˙x=0˙y=0˙
43 2 42 syl5bb RCRing0˙LIdealR0˙BaseRxBaseRyBaseRxRy0˙x0˙y0˙RNzRingxBaseRyBaseRxRy=0˙x=0˙y=0˙
44 43 pm5.32i RCRing0˙LIdealR0˙BaseRxBaseRyBaseRxRy0˙x0˙y0˙RCRingRNzRingxBaseRyBaseRxRy=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=CRingDomn
49 48 eleq2i RIDomnRCRingDomn
50 elin RCRingDomnRCRingRDomn
51 8 45 1 isdomn RDomnRNzRingxBaseRyBaseRxRy=0˙x=0˙y=0˙
52 51 anbi2i RCRingRDomnRCRingRNzRingxBaseRyBaseRxRy=0˙x=0˙y=0˙
53 49 50 52 3bitri RIDomnRCRingRNzRingxBaseRyBaseRxRy=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 |-