Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isfldidl Structured version   Visualization version   Unicode version

Theorem isfldidl 32294
Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypotheses
Ref Expression
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
Ref Expression
isfldidl  |-  ( K  e.  Fld  <->  ( K  e. CRingOps 
/\  U  =/=  Z  /\  ( Idl `  K
)  =  { { Z } ,  X }
) )

Proof of Theorem isfldidl
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fldcrng 32230 . . 3  |-  ( K  e.  Fld  ->  K  e. CRingOps )
2 flddivrng 26136 . . . 4  |-  ( K  e.  Fld  ->  K  e. 
DivRingOps )
3 isfldidl.1 . . . . 5  |-  G  =  ( 1st `  K
)
4 isfldidl.2 . . . . 5  |-  H  =  ( 2nd `  K
)
5 isfldidl.3 . . . . 5  |-  X  =  ran  G
6 isfldidl.4 . . . . 5  |-  Z  =  (GId `  G )
7 isfldidl.5 . . . . 5  |-  U  =  (GId `  H )
83, 4, 5, 6, 7dvrunz 26154 . . . 4  |-  ( K  e.  DivRingOps  ->  U  =/=  Z
)
92, 8syl 17 . . 3  |-  ( K  e.  Fld  ->  U  =/=  Z )
103, 4, 5, 6divrngidl 32254 . . . 4  |-  ( K  e.  DivRingOps  ->  ( Idl `  K
)  =  { { Z } ,  X }
)
112, 10syl 17 . . 3  |-  ( K  e.  Fld  ->  ( Idl `  K )  =  { { Z } ,  X } )
121, 9, 113jca 1187 . 2  |-  ( K  e.  Fld  ->  ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } ) )
13 crngorngo 32226 . . . . . 6  |-  ( K  e. CRingOps  ->  K  e.  RingOps )
14133ad2ant1 1028 . . . . 5  |-  ( ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  K  e.  RingOps )
15 simp2 1008 . . . . 5  |-  ( ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  U  =/=  Z )
163rneqi 5060 . . . . . . . . . . . . . . 15  |-  ran  G  =  ran  ( 1st `  K
)
175, 16eqtri 2472 . . . . . . . . . . . . . 14  |-  X  =  ran  ( 1st `  K
)
1817, 4, 7rngo1cl 26150 . . . . . . . . . . . . 13  |-  ( K  e.  RingOps  ->  U  e.  X
)
1913, 18syl 17 . . . . . . . . . . . 12  |-  ( K  e. CRingOps  ->  U  e.  X
)
2019ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  /\  x  e.  ( X  \  { Z } ) )  ->  U  e.  X )
21 eldif 3413 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( X  \  { Z } )  <->  ( x  e.  X  /\  -.  x  e.  { Z } ) )
22 snssi 4115 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  X  ->  { x }  C_  X )
233, 5igenss 32288 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  RingOps  /\  {
x }  C_  X
)  ->  { x }  C_  ( K  IdlGen  { x } ) )
2422, 23sylan2 477 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  RingOps  /\  x  e.  X )  ->  { x }  C_  ( K  IdlGen  { x } ) )
25 vex 3047 . . . . . . . . . . . . . . . . . . . . . 22  |-  x  e. 
_V
2625snss 4095 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( K  IdlGen  { x } )  <->  { x }  C_  ( K  IdlGen  { x } ) )
2726biimpri 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( { x }  C_  ( K  IdlGen  { x }
)  ->  x  e.  ( K  IdlGen  { x } ) )
28 eleq2 2517 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K  IdlGen  { x }
)  =  { Z }  ->  ( x  e.  ( K  IdlGen  { x } )  <->  x  e.  { Z } ) )
2927, 28syl5ibcom 224 . . . . . . . . . . . . . . . . . . 19  |-  ( { x }  C_  ( K  IdlGen  { x }
)  ->  ( ( K  IdlGen  { x }
)  =  { Z }  ->  x  e.  { Z } ) )
3029con3dimp 443 . . . . . . . . . . . . . . . . . 18  |-  ( ( { x }  C_  ( K  IdlGen  { x } )  /\  -.  x  e.  { Z } )  ->  -.  ( K  IdlGen  { x } )  =  { Z } )
3124, 30sylan 474 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  RingOps  /\  x  e.  X )  /\  -.  x  e.  { Z } )  ->  -.  ( K  IdlGen  { x } )  =  { Z } )
3231anasss 652 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  RingOps  /\  (
x  e.  X  /\  -.  x  e.  { Z } ) )  ->  -.  ( K  IdlGen  { x } )  =  { Z } )
3321, 32sylan2b 478 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  RingOps  /\  x  e.  ( X  \  { Z } ) )  ->  -.  ( K  IdlGen  { x } )  =  { Z } )
3433adantlr 720 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  RingOps  /\  ( Idl `  K )  =  { { Z } ,  X }
)  /\  x  e.  ( X  \  { Z } ) )  ->  -.  ( K  IdlGen  { x } )  =  { Z } )
35 eldifi 3554 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( X  \  { Z } )  ->  x  e.  X )
3635snssd 4116 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( X  \  { Z } )  ->  { x }  C_  X )
373, 5igenidl 32289 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( K  e.  RingOps  /\  {
x }  C_  X
)  ->  ( K  IdlGen  { x } )  e.  ( Idl `  K
) )
3836, 37sylan2 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( K  e.  RingOps  /\  x  e.  ( X  \  { Z } ) )  -> 
( K  IdlGen  { x } )  e.  ( Idl `  K ) )
39 eleq2 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Idl `  K )  =  { { Z } ,  X }  ->  ( ( K  IdlGen  { x } )  e.  ( Idl `  K
)  <->  ( K  IdlGen  { x } )  e. 
{ { Z } ,  X } ) )
4038, 39syl5ibcom 224 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  RingOps  /\  x  e.  ( X  \  { Z } ) )  -> 
( ( Idl `  K
)  =  { { Z } ,  X }  ->  ( K  IdlGen  { x } )  e.  { { Z } ,  X } ) )
4140imp 431 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  RingOps  /\  x  e.  ( X  \  { Z } ) )  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  ( K  IdlGen  { x }
)  e.  { { Z } ,  X }
)
4241an32s 812 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  RingOps  /\  ( Idl `  K )  =  { { Z } ,  X }
)  /\  x  e.  ( X  \  { Z } ) )  -> 
( K  IdlGen  { x } )  e.  { { Z } ,  X } )
43 ovex 6316 . . . . . . . . . . . . . . . . 17  |-  ( K 
IdlGen  { x } )  e.  _V
4443elpr 3985 . . . . . . . . . . . . . . . 16  |-  ( ( K  IdlGen  { x }
)  e.  { { Z } ,  X }  <->  ( ( K  IdlGen  { x } )  =  { Z }  \/  ( K  IdlGen  { x }
)  =  X ) )
4542, 44sylib 200 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  RingOps  /\  ( Idl `  K )  =  { { Z } ,  X }
)  /\  x  e.  ( X  \  { Z } ) )  -> 
( ( K  IdlGen  { x } )  =  { Z }  \/  ( K  IdlGen  { x } )  =  X ) )
4645ord 379 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  RingOps  /\  ( Idl `  K )  =  { { Z } ,  X }
)  /\  x  e.  ( X  \  { Z } ) )  -> 
( -.  ( K 
IdlGen  { x } )  =  { Z }  ->  ( K  IdlGen  { x } )  =  X ) )
4734, 46mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  RingOps  /\  ( Idl `  K )  =  { { Z } ,  X }
)  /\  x  e.  ( X  \  { Z } ) )  -> 
( K  IdlGen  { x } )  =  X )
4813, 47sylanl1 655 . . . . . . . . . . . 12  |-  ( ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  /\  x  e.  ( X  \  { Z } ) )  ->  ( K  IdlGen  { x } )  =  X )
493, 4, 5prnc 32293 . . . . . . . . . . . . . 14  |-  ( ( K  e. CRingOps  /\  x  e.  X )  ->  ( K  IdlGen  { x }
)  =  { z  e.  X  |  E. y  e.  X  z  =  ( y H x ) } )
5035, 49sylan2 477 . . . . . . . . . . . . 13  |-  ( ( K  e. CRingOps  /\  x  e.  ( X  \  { Z } ) )  -> 
( K  IdlGen  { x } )  =  {
z  e.  X  |  E. y  e.  X  z  =  ( y H x ) } )
5150adantlr 720 . . . . . . . . . . . 12  |-  ( ( ( 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 ) } )
5248, 51eqtr3d 2486 . . . . . . . . . . 11  |-  ( ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  /\  x  e.  ( X  \  { Z } ) )  ->  X  =  { z  e.  X  |  E. y  e.  X  z  =  ( y H x ) } )
5320, 52eleqtrd 2530 . . . . . . . . . 10  |-  ( ( ( 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 2454 . . . . . . . . . . . 12  |-  ( z  =  U  ->  (
z  =  ( y H x )  <->  U  =  ( y H x ) ) )
5554rexbidv 2900 . . . . . . . . . . 11  |-  ( z  =  U  ->  ( E. y  e.  X  z  =  ( y H x )  <->  E. y  e.  X  U  =  ( y H x ) ) )
5655elrab 3195 . . . . . . . . . 10  |-  ( U  e.  { z  e.  X  |  E. y  e.  X  z  =  ( y H x ) }  <->  ( U  e.  X  /\  E. y  e.  X  U  =  ( y H x ) ) )
5753, 56sylib 200 . . . . . . . . 9  |-  ( ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  /\  x  e.  ( X  \  { Z } ) )  ->  ( U  e.  X  /\  E. y  e.  X  U  =  ( y H x ) ) )
5857simprd 465 . . . . . . . 8  |-  ( ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  /\  x  e.  ( X  \  { Z } ) )  ->  E. y  e.  X  U  =  ( y H x ) )
59 eqcom 2457 . . . . . . . . 9  |-  ( ( y H x )  =  U  <->  U  =  ( y H x ) )
6059rexbii 2888 . . . . . . . 8  |-  ( E. y  e.  X  ( y H x )  =  U  <->  E. y  e.  X  U  =  ( y H x ) )
6158, 60sylibr 216 . . . . . . 7  |-  ( ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  /\  x  e.  ( X  \  { Z } ) )  ->  E. y  e.  X  ( y H x )  =  U )
6261ralrimiva 2801 . . . . . 6  |-  ( ( K  e. CRingOps  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  A. x  e.  ( X  \  { Z }
) E. y  e.  X  ( y H x )  =  U )
63623adant2 1026 . . . . 5  |-  ( ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  A. x  e.  ( X  \  { Z } ) E. y  e.  X  ( y H x )  =  U )
6414, 15, 63jca32 538 . . . 4  |-  ( ( 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 ) ) )
653, 4, 6, 5, 7isdrngo3 32191 . . . 4  |-  ( K  e.  DivRingOps 
<->  ( K  e.  RingOps  /\  ( U  =/=  Z  /\  A. x  e.  ( X  \  { Z } ) E. y  e.  X  ( y H x )  =  U ) ) )
6664, 65sylibr 216 . . 3  |-  ( ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  K  e. 
DivRingOps )
67 simp1 1007 . . 3  |-  ( ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  K  e. CRingOps )
68 isfld2 32231 . . 3  |-  ( K  e.  Fld  <->  ( K  e. 
DivRingOps 
/\  K  e. CRingOps )
)
6966, 67, 68sylanbrc 669 . 2  |-  ( ( K  e. CRingOps  /\  U  =/= 
Z  /\  ( Idl `  K )  =  { { Z } ,  X } )  ->  K  e.  Fld )
7012, 69impbii 191 1  |-  ( K  e.  Fld  <->  ( K  e. CRingOps 
/\  U  =/=  Z  /\  ( Idl `  K
)  =  { { Z } ,  X }
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188    \/ wo 370    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886    =/= wne 2621   A.wral 2736   E.wrex 2737   {crab 2740    \ cdif 3400    C_ wss 3403   {csn 3967   {cpr 3969   ran crn 4834   ` cfv 5581  (class class class)co 6288   1stc1st 6788   2ndc2nd 6789  GIdcgi 25908   RingOpscrngo 26096   DivRingOpscdrng 26126   Fldcfld 26134  CRingOpsccring 32221   Idlcidl 32233    IdlGen cigen 32285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-1o 7179  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-grpo 25912  df-gid 25913  df-ginv 25914  df-ablo 26003  df-ass 26034  df-exid 26036  df-mgmOLD 26040  df-sgrOLD 26052  df-mndo 26059  df-rngo 26097  df-drngo 26127  df-com2 26132  df-fld 26135  df-crngo 32222  df-idl 32236  df-igen 32286
This theorem is referenced by:  isfldidl2  32295
  Copyright terms: Public domain W3C validator