This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isfldidl2

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

Ref Expression
Hypotheses isfldidl2.1 
|- G = ( 1st ` K )
isfldidl2.2 
|- H = ( 2nd ` K )
isfldidl2.3 
|- X = ran G
isfldidl2.4 
|- Z = ( GId ` G )
Assertion isfldidl2 
|- ( K e. Fld <-> ( K e. CRingOps /\ X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) )

Proof

Step Hyp Ref Expression
1 isfldidl2.1 
 |-  G = ( 1st ` K )
2 isfldidl2.2 
 |-  H = ( 2nd ` K )
3 isfldidl2.3 
 |-  X = ran G
4 isfldidl2.4 
 |-  Z = ( GId ` G )
5 eqid 
 |-  ( GId ` H ) = ( GId ` H )
6 1 2 3 4 5 isfldidl 
 |-  ( K e. Fld <-> ( K e. CRingOps /\ ( GId ` H ) =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )
7 crngorngo 
 |-  ( K e. CRingOps -> K e. RingOps )
8 eqcom 
 |-  ( ( GId ` H ) = Z <-> Z = ( GId ` H ) )
9 1 2 3 4 5 0rngo 
 |-  ( K e. RingOps -> ( Z = ( GId ` H ) <-> X = { Z } ) )
10 8 9 bitrid 
 |-  ( K e. RingOps -> ( ( GId ` H ) = Z <-> X = { Z } ) )
11 7 10 syl 
 |-  ( K e. CRingOps -> ( ( GId ` H ) = Z <-> X = { Z } ) )
12 11 necon3bid 
 |-  ( K e. CRingOps -> ( ( GId ` H ) =/= Z <-> X =/= { Z } ) )
13 12 anbi1d 
 |-  ( K e. CRingOps -> ( ( ( GId ` H ) =/= Z /\ ( Idl ` K ) = { { Z } , X } ) <-> ( X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) ) )
14 13 pm5.32i 
 |-  ( ( K e. CRingOps /\ ( ( GId ` H ) =/= Z /\ ( Idl ` K ) = { { Z } , X } ) ) <-> ( K e. CRingOps /\ ( X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) ) )
15 3anass 
 |-  ( ( K e. CRingOps /\ ( GId ` H ) =/= Z /\ ( Idl ` K ) = { { Z } , X } ) <-> ( K e. CRingOps /\ ( ( GId ` H ) =/= Z /\ ( Idl ` K ) = { { Z } , X } ) ) )
16 3anass 
 |-  ( ( K e. CRingOps /\ X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) <-> ( K e. CRingOps /\ ( X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) ) )
17 14 15 16 3bitr4i 
 |-  ( ( K e. CRingOps /\ ( GId ` H ) =/= Z /\ ( Idl ` K ) = { { Z } , X } ) <-> ( K e. CRingOps /\ X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) )
18 6 17 bitri 
 |-  ( K e. Fld <-> ( K e. CRingOps /\ X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) )