Metamath Proof Explorer

Theorem isfieldidl2

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

Ref Expression
Hypotheses isfieldidl.b 
|- B = ( Base ` R )
isfieldidl.0 
|- .0. = ( 0g ` R )
isfieldidl.i 
|- I = ( LIdeal ` R )
Assertion isfieldidl2 
|- ( R e. Field <-> ( R e. CRing /\ B =/= { .0. } /\ 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 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 1 2 3 4 isfieldidl 
 |-  ( R e. Field <-> ( R e. CRing /\ .0. =/= ( 1r ` R ) /\ I = { { .0. } , B } ) )
6 crngring 
 |-  ( R e. CRing -> R e. Ring )
7 eqcom 
 |-  ( .0. = ( 1r ` R ) <-> ( 1r ` R ) = .0. )
8 1 2 4 0ring01eqbi2 
 |-  ( R e. Ring -> ( B = { .0. } <-> ( 1r ` R ) = .0. ) )
9 7 8 bitr4id 
 |-  ( R e. Ring -> ( .0. = ( 1r ` R ) <-> B = { .0. } ) )
10 6 9 syl 
 |-  ( R e. CRing -> ( .0. = ( 1r ` R ) <-> B = { .0. } ) )
11 10 necon3bid 
 |-  ( R e. CRing -> ( .0. =/= ( 1r ` R ) <-> B =/= { .0. } ) )
12 11 anbi1d 
 |-  ( R e. CRing -> ( ( .0. =/= ( 1r ` R ) /\ I = { { .0. } , B } ) <-> ( B =/= { .0. } /\ I = { { .0. } , B } ) ) )
13 12 pm5.32i 
 |-  ( ( R e. CRing /\ ( .0. =/= ( 1r ` R ) /\ I = { { .0. } , B } ) ) <-> ( R e. CRing /\ ( B =/= { .0. } /\ I = { { .0. } , B } ) ) )
14 3anass 
 |-  ( ( R e. CRing /\ .0. =/= ( 1r ` R ) /\ I = { { .0. } , B } ) <-> ( R e. CRing /\ ( .0. =/= ( 1r ` R ) /\ I = { { .0. } , B } ) ) )
15 3anass 
 |-  ( ( R e. CRing /\ B =/= { .0. } /\ I = { { .0. } , B } ) <-> ( R e. CRing /\ ( B =/= { .0. } /\ I = { { .0. } , B } ) ) )
16 13 14 15 3bitr4i 
 |-  ( ( R e. CRing /\ .0. =/= ( 1r ` R ) /\ I = { { .0. } , B } ) <-> ( R e. CRing /\ B =/= { .0. } /\ I = { { .0. } , B } ) )
17 5 16 bitri 
 |-  ( R e. Field <-> ( R e. CRing /\ B =/= { .0. } /\ I = { { .0. } , B } ) )