Metamath Proof Explorer

Theorem isfieldidl

Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by AV, 30-Jun-2026)

Ref Expression
Hypotheses isfieldidl.b 
|- B = ( Base ` R )
isfieldidl.0 
|- .0. = ( 0g ` R )
isfieldidl.i 
|- I = ( LIdeal ` R )
isfieldidl.1 
|- .1. = ( 1r ` R )
Assertion isfieldidl 
|- ( R e. Field <-> ( R e. CRing /\ .0. =/= .1. /\ I = { { .0. } , B } ) )

Proof

Step Hyp Ref Expression
1 isfieldidl.b 
 |-  B = ( Base ` R )
2 isfieldidl.0 
 |-  .0. = ( 0g ` R )
3 isfieldidl.i 
 |-  I = ( LIdeal ` R )
4 isfieldidl.1 
 |-  .1. = ( 1r ` R )
5 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
6 1 2 3 drngidl 
 |-  ( R e. NzRing -> ( R e. DivRing <-> I = { { .0. } , B } ) )
7 6 adantr 
 |-  ( ( R e. NzRing /\ R e. CRing ) -> ( R e. DivRing <-> I = { { .0. } , B } ) )
8 4 2 nzrnz 
 |-  ( R e. NzRing -> .1. =/= .0. )
9 8 necomd 
 |-  ( R e. NzRing -> .0. =/= .1. )
10 9 a1d 
 |-  ( R e. NzRing -> ( I = { { .0. } , B } -> .0. =/= .1. ) )
11 10 adantr 
 |-  ( ( R e. NzRing /\ R e. CRing ) -> ( I = { { .0. } , B } -> .0. =/= .1. ) )
12 11 pm4.71rd 
 |-  ( ( R e. NzRing /\ R e. CRing ) -> ( I = { { .0. } , B } <-> ( .0. =/= .1. /\ I = { { .0. } , B } ) ) )
13 7 12 bitrd 
 |-  ( ( R e. NzRing /\ R e. CRing ) -> ( R e. DivRing <-> ( .0. =/= .1. /\ I = { { .0. } , B } ) ) )
14 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
15 14 con3i 
 |-  ( -. R e. NzRing -> -. R e. DivRing )
16 15 adantr 
 |-  ( ( -. R e. NzRing /\ R e. CRing ) -> -. R e. DivRing )
17 ianor 
 |-  ( -. ( R e. Ring /\ .1. =/= .0. ) <-> ( -. R e. Ring \/ -. .1. =/= .0. ) )
18 4 2 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ .1. =/= .0. ) )
19 17 18 xchnxbir 
 |-  ( -. R e. NzRing <-> ( -. R e. Ring \/ -. .1. =/= .0. ) )
20 pm2.24 
 |-  ( R e. Ring -> ( -. R e. Ring -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) ) )
21 crngring 
 |-  ( R e. CRing -> R e. Ring )
22 20 21 syl11 
 |-  ( -. R e. Ring -> ( R e. CRing -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) ) )
23 id 
 |-  ( .0. =/= .1. -> .0. =/= .1. )
24 23 necomd 
 |-  ( .0. =/= .1. -> .1. =/= .0. )
25 24 con3i 
 |-  ( -. .1. =/= .0. -> -. .0. =/= .1. )
26 25 orcd 
 |-  ( -. .1. =/= .0. -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) )
27 26 a1d 
 |-  ( -. .1. =/= .0. -> ( R e. CRing -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) ) )
28 22 27 jaoi 
 |-  ( ( -. R e. Ring \/ -. .1. =/= .0. ) -> ( R e. CRing -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) ) )
29 19 28 sylbi 
 |-  ( -. R e. NzRing -> ( R e. CRing -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) ) )
30 29 imp 
 |-  ( ( -. R e. NzRing /\ R e. CRing ) -> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) )
31 ianor 
 |-  ( -. ( .0. =/= .1. /\ I = { { .0. } , B } ) <-> ( -. .0. =/= .1. \/ -. I = { { .0. } , B } ) )
32 30 31 sylibr 
 |-  ( ( -. R e. NzRing /\ R e. CRing ) -> -. ( .0. =/= .1. /\ I = { { .0. } , B } ) )
33 16 32 2falsed 
 |-  ( ( -. R e. NzRing /\ R e. CRing ) -> ( R e. DivRing <-> ( .0. =/= .1. /\ I = { { .0. } , B } ) ) )
34 13 33 pm2.61ian 
 |-  ( R e. CRing -> ( R e. DivRing <-> ( .0. =/= .1. /\ I = { { .0. } , B } ) ) )
35 34 pm5.32i 
 |-  ( ( R e. CRing /\ R e. DivRing ) <-> ( R e. CRing /\ ( .0. =/= .1. /\ I = { { .0. } , B } ) ) )
36 ancom 
 |-  ( ( R e. DivRing /\ R e. CRing ) <-> ( R e. CRing /\ R e. DivRing ) )
37 3anass 
 |-  ( ( R e. CRing /\ .0. =/= .1. /\ I = { { .0. } , B } ) <-> ( R e. CRing /\ ( .0. =/= .1. /\ I = { { .0. } , B } ) ) )
38 35 36 37 3bitr4i 
 |-  ( ( R e. DivRing /\ R e. CRing ) <-> ( R e. CRing /\ .0. =/= .1. /\ I = { { .0. } , B } ) )
39 5 38 bitri 
 |-  ( R e. Field <-> ( R e. CRing /\ .0. =/= .1. /\ I = { { .0. } , B } ) )