Metamath Proof Explorer

Theorem isfldidl

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

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

Proof

Step Hyp Ref Expression
1 isfldidl.1 
 |-  G = ( 1st ` K )
2 isfldidl.2 
 |-  H = ( 2nd ` K )
3 isfldidl.3 
 |-  X = ran G
4 isfldidl.4 
 |-  Z = ( GId ` G )
5 isfldidl.5 
 |-  U = ( GId ` H )
6 fldcrng 
 |-  ( K e. Fld -> K e. CRingOps )
7 flddivrng 
 |-  ( K e. Fld -> K e. DivRingOps )
8 1 2 3 4 5 dvrunz 
 |-  ( K e. DivRingOps -> U =/= Z )
9 7 8 syl 
 |-  ( K e. Fld -> U =/= Z )
10 1 2 3 4 divrngidl 
 |-  ( K e. DivRingOps -> ( Idl ` K ) = { { Z } , X } )
11 7 10 syl 
 |-  ( K e. Fld -> ( Idl ` K ) = { { Z } , X } )
12 6 9 11 3jca 
 |-  ( K e. Fld -> ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )
13 crngorngo 
 |-  ( K e. CRingOps -> K e. RingOps )
14 13 3ad2ant1 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. RingOps )
15 simp2 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> U =/= Z )
16 1 rneqi 
 |-  ran G = ran ( 1st ` K )
17 3 16 eqtri 
 |-  X = ran ( 1st ` K )
18 17 2 5 rngo1cl 
 |-  ( K e. RingOps -> U e. X )
19 13 18 syl 
 |-  ( K e. CRingOps -> U e. X )
20 19 ad2antrr 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> U e. X )
21 eldif 
 |-  ( x e. ( X \ { Z } ) <-> ( x e. X /\ -. x e. { Z } ) )
22 snssi 
 |-  ( x e. X -> { x } C_ X )
23 1 3 igenss 
 |-  ( ( K e. RingOps /\ { x } C_ X ) -> { x } C_ ( K IdlGen { x } ) )
24 22 23 sylan2 
 |-  ( ( K e. RingOps /\ x e. X ) -> { x } C_ ( K IdlGen { x } ) )
25 vex 
 |-  x e. _V
26 25 snss 
 |-  ( x e. ( K IdlGen { x } ) <-> { x } C_ ( K IdlGen { x } ) )
27 26 biimpri 
 |-  ( { x } C_ ( K IdlGen { x } ) -> x e. ( K IdlGen { x } ) )
28 eleq2 
 |-  ( ( K IdlGen { x } ) = { Z } -> ( x e. ( K IdlGen { x } ) <-> x e. { Z } ) )
29 27 28 syl5ibcom 
 |-  ( { x } C_ ( K IdlGen { x } ) -> ( ( K IdlGen { x } ) = { Z } -> x e. { Z } ) )
30 29 con3dimp 
 |-  ( ( { x } C_ ( K IdlGen { x } ) /\ -. x e. { Z } ) -> -. ( K IdlGen { x } ) = { Z } )
31 24 30 sylan 
 |-  ( ( ( K e. RingOps /\ x e. X ) /\ -. x e. { Z } ) -> -. ( K IdlGen { x } ) = { Z } )
32 31 anasss 
 |-  ( ( K e. RingOps /\ ( x e. X /\ -. x e. { Z } ) ) -> -. ( K IdlGen { x } ) = { Z } )
33 21 32 sylan2b 
 |-  ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) -> -. ( K IdlGen { x } ) = { Z } )
34 33 adantlr 
 |-  ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> -. ( K IdlGen { x } ) = { Z } )
35 eldifi 
 |-  ( x e. ( X \ { Z } ) -> x e. X )
36 35 snssd 
 |-  ( x e. ( X \ { Z } ) -> { x } C_ X )
37 1 3 igenidl 
 |-  ( ( K e. RingOps /\ { x } C_ X ) -> ( K IdlGen { x } ) e. ( Idl ` K ) )
38 36 37 sylan2 
 |-  ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) e. ( Idl ` K ) )
39 eleq2 
 |-  ( ( Idl ` K ) = { { Z } , X } -> ( ( K IdlGen { x } ) e. ( Idl ` K ) <-> ( K IdlGen { x } ) e. { { Z } , X } ) )
40 38 39 syl5ibcom 
 |-  ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) -> ( ( Idl ` K ) = { { Z } , X } -> ( K IdlGen { x } ) e. { { Z } , X } ) )
41 40 imp 
 |-  ( ( ( K e. RingOps /\ x e. ( X \ { Z } ) ) /\ ( Idl ` K ) = { { Z } , X } ) -> ( K IdlGen { x } ) e. { { Z } , X } )
42 41 an32s 
 |-  ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) e. { { Z } , X } )
43 ovex 
 |-  ( K IdlGen { x } ) e. _V
44 43 elpr 
 |-  ( ( K IdlGen { x } ) e. { { Z } , X } <-> ( ( K IdlGen { x } ) = { Z } \/ ( K IdlGen { x } ) = X ) )
45 42 44 sylib 
 |-  ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( ( K IdlGen { x } ) = { Z } \/ ( K IdlGen { x } ) = X ) )
46 45 ord 
 |-  ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( -. ( K IdlGen { x } ) = { Z } -> ( K IdlGen { x } ) = X ) )
47 34 46 mpd 
 |-  ( ( ( K e. RingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = X )
48 13 47 sylanl1 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = X )
49 1 2 3 prnc 
 |-  ( ( K e. CRingOps /\ x e. X ) -> ( K IdlGen { x } ) = { z e. X | E. y e. X z = ( y H x ) } )
50 35 49 sylan2 
 |-  ( ( K e. CRingOps /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = { z e. X | E. y e. X z = ( y H x ) } )
51 50 adantlr 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( K IdlGen { x } ) = { z e. X | E. y e. X z = ( y H x ) } )
52 48 51 eqtr3d 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> X = { z e. X | E. y e. X z = ( y H x ) } )
53 20 52 eleqtrd 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> U e. { z e. X | E. y e. X z = ( y H x ) } )
54 eqeq1 
 |-  ( z = U -> ( z = ( y H x ) <-> U = ( y H x ) ) )
55 54 rexbidv 
 |-  ( z = U -> ( E. y e. X z = ( y H x ) <-> E. y e. X U = ( y H x ) ) )
56 55 elrab 
 |-  ( U e. { z e. X | E. y e. X z = ( y H x ) } <-> ( U e. X /\ E. y e. X U = ( y H x ) ) )
57 53 56 sylib 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> ( U e. X /\ E. y e. X U = ( y H x ) ) )
58 57 simprd 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> E. y e. X U = ( y H x ) )
59 eqcom 
 |-  ( ( y H x ) = U <-> U = ( y H x ) )
60 59 rexbii 
 |-  ( E. y e. X ( y H x ) = U <-> E. y e. X U = ( y H x ) )
61 58 60 sylibr 
 |-  ( ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) /\ x e. ( X \ { Z } ) ) -> E. y e. X ( y H x ) = U )
62 61 ralrimiva 
 |-  ( ( K e. CRingOps /\ ( Idl ` K ) = { { Z } , X } ) -> A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U )
63 62 3adant2 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U )
64 14 15 63 jca32 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> ( K e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
65 1 2 4 3 5 isdrngo3 
 |-  ( K e. DivRingOps <-> ( K e. RingOps /\ ( U =/= Z /\ A. x e. ( X \ { Z } ) E. y e. X ( y H x ) = U ) ) )
66 64 65 sylibr 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. DivRingOps )
67 simp1 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. CRingOps )
68 isfld2 
 |-  ( K e. Fld <-> ( K e. DivRingOps /\ K e. CRingOps ) )
69 66 67 68 sylanbrc 
 |-  ( ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) -> K e. Fld )
70 12 69 impbii 
 |-  ( K e. Fld <-> ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )