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	syl5bb	|- ( 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 } ) )