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

Theorem isfldidl 36741
Description: Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)
Hypotheses
Ref Expression
isfldidl.1 𝐺 = (1st𝐾)
isfldidl.2 𝐻 = (2nd𝐾)
isfldidl.3 𝑋 = ran 𝐺
isfldidl.4 𝑍 = (GId‘𝐺)
isfldidl.5 𝑈 = (GId‘𝐻)
Assertion
Ref Expression
isfldidl (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))

Proof of Theorem isfldidl
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fldcrngo 36677 . . 3 (𝐾 ∈ Fld → 𝐾 ∈ CRingOps)
2 flddivrng 36672 . . . 4 (𝐾 ∈ Fld → 𝐾 ∈ DivRingOps)
3 isfldidl.1 . . . . 5 𝐺 = (1st𝐾)
4 isfldidl.2 . . . . 5 𝐻 = (2nd𝐾)
5 isfldidl.3 . . . . 5 𝑋 = ran 𝐺
6 isfldidl.4 . . . . 5 𝑍 = (GId‘𝐺)
7 isfldidl.5 . . . . 5 𝑈 = (GId‘𝐻)
83, 4, 5, 6, 7dvrunz 36627 . . . 4 (𝐾 ∈ DivRingOps → 𝑈𝑍)
92, 8syl 17 . . 3 (𝐾 ∈ Fld → 𝑈𝑍)
103, 4, 5, 6divrngidl 36701 . . . 4 (𝐾 ∈ DivRingOps → (Idl‘𝐾) = {{𝑍}, 𝑋})
112, 10syl 17 . . 3 (𝐾 ∈ Fld → (Idl‘𝐾) = {{𝑍}, 𝑋})
121, 9, 113jca 1128 . 2 (𝐾 ∈ Fld → (𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
13 crngorngo 36673 . . . . . 6 (𝐾 ∈ CRingOps → 𝐾 ∈ RingOps)
14133ad2ant1 1133 . . . . 5 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ RingOps)
15 simp2 1137 . . . . 5 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝑈𝑍)
163rneqi 5928 . . . . . . . . . . . . . . 15 ran 𝐺 = ran (1st𝐾)
175, 16eqtri 2759 . . . . . . . . . . . . . 14 𝑋 = ran (1st𝐾)
1817, 4, 7rngo1cl 36612 . . . . . . . . . . . . 13 (𝐾 ∈ RingOps → 𝑈𝑋)
1913, 18syl 17 . . . . . . . . . . . 12 (𝐾 ∈ CRingOps → 𝑈𝑋)
2019ad2antrr 724 . . . . . . . . . . 11 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑈𝑋)
21 eldif 3954 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑋 ∖ {𝑍}) ↔ (𝑥𝑋 ∧ ¬ 𝑥 ∈ {𝑍}))
22 snssi 4804 . . . . . . . . . . . . . . . . . . 19 (𝑥𝑋 → {𝑥} ⊆ 𝑋)
233, 5igenss 36735 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ RingOps ∧ {𝑥} ⊆ 𝑋) → {𝑥} ⊆ (𝐾 IdlGen {𝑥}))
2422, 23sylan2 593 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ RingOps ∧ 𝑥𝑋) → {𝑥} ⊆ (𝐾 IdlGen {𝑥}))
25 vex 3477 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 ∈ V
2625snss 4782 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐾 IdlGen {𝑥}) ↔ {𝑥} ⊆ (𝐾 IdlGen {𝑥}))
2726biimpri 227 . . . . . . . . . . . . . . . . . . . 20 ({𝑥} ⊆ (𝐾 IdlGen {𝑥}) → 𝑥 ∈ (𝐾 IdlGen {𝑥}))
28 eleq2 2821 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 IdlGen {𝑥}) = {𝑍} → (𝑥 ∈ (𝐾 IdlGen {𝑥}) ↔ 𝑥 ∈ {𝑍}))
2927, 28syl5ibcom 244 . . . . . . . . . . . . . . . . . . 19 ({𝑥} ⊆ (𝐾 IdlGen {𝑥}) → ((𝐾 IdlGen {𝑥}) = {𝑍} → 𝑥 ∈ {𝑍}))
3029con3dimp 409 . . . . . . . . . . . . . . . . . 18 (({𝑥} ⊆ (𝐾 IdlGen {𝑥}) ∧ ¬ 𝑥 ∈ {𝑍}) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
3124, 30sylan 580 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ RingOps ∧ 𝑥𝑋) ∧ ¬ 𝑥 ∈ {𝑍}) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
3231anasss 467 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ RingOps ∧ (𝑥𝑋 ∧ ¬ 𝑥 ∈ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
3321, 32sylan2b 594 . . . . . . . . . . . . . . 15 ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
3433adantlr 713 . . . . . . . . . . . . . 14 (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ¬ (𝐾 IdlGen {𝑥}) = {𝑍})
35 eldifi 4122 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝑋 ∖ {𝑍}) → 𝑥𝑋)
3635snssd 4805 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑋 ∖ {𝑍}) → {𝑥} ⊆ 𝑋)
373, 5igenidl 36736 . . . . . . . . . . . . . . . . . . . 20 ((𝐾 ∈ RingOps ∧ {𝑥} ⊆ 𝑋) → (𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾))
3836, 37sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾))
39 eleq2 2821 . . . . . . . . . . . . . . . . . . 19 ((Idl‘𝐾) = {{𝑍}, 𝑋} → ((𝐾 IdlGen {𝑥}) ∈ (Idl‘𝐾) ↔ (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋}))
4038, 39syl5ibcom 244 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ((Idl‘𝐾) = {{𝑍}, 𝑋} → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋}))
4140imp 407 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ RingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋})
4241an32s 650 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋})
43 ovex 7426 . . . . . . . . . . . . . . . . 17 (𝐾 IdlGen {𝑥}) ∈ V
4443elpr 4645 . . . . . . . . . . . . . . . 16 ((𝐾 IdlGen {𝑥}) ∈ {{𝑍}, 𝑋} ↔ ((𝐾 IdlGen {𝑥}) = {𝑍} ∨ (𝐾 IdlGen {𝑥}) = 𝑋))
4542, 44sylib 217 . . . . . . . . . . . . . . 15 (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ((𝐾 IdlGen {𝑥}) = {𝑍} ∨ (𝐾 IdlGen {𝑥}) = 𝑋))
4645ord 862 . . . . . . . . . . . . . 14 (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (¬ (𝐾 IdlGen {𝑥}) = {𝑍} → (𝐾 IdlGen {𝑥}) = 𝑋))
4734, 46mpd 15 . . . . . . . . . . . . 13 (((𝐾 ∈ RingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = 𝑋)
4813, 47sylanl1 678 . . . . . . . . . . . 12 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = 𝑋)
493, 4, 5prnc 36740 . . . . . . . . . . . . . 14 ((𝐾 ∈ CRingOps ∧ 𝑥𝑋) → (𝐾 IdlGen {𝑥}) = {𝑧𝑋 ∣ ∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥)})
5035, 49sylan2 593 . . . . . . . . . . . . 13 ((𝐾 ∈ CRingOps ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = {𝑧𝑋 ∣ ∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥)})
5150adantlr 713 . . . . . . . . . . . 12 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝐾 IdlGen {𝑥}) = {𝑧𝑋 ∣ ∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥)})
5248, 51eqtr3d 2773 . . . . . . . . . . 11 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑋 = {𝑧𝑋 ∣ ∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥)})
5320, 52eleqtrd 2834 . . . . . . . . . 10 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → 𝑈 ∈ {𝑧𝑋 ∣ ∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥)})
54 eqeq1 2735 . . . . . . . . . . . 12 (𝑧 = 𝑈 → (𝑧 = (𝑦𝐻𝑥) ↔ 𝑈 = (𝑦𝐻𝑥)))
5554rexbidv 3177 . . . . . . . . . . 11 (𝑧 = 𝑈 → (∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥) ↔ ∃𝑦𝑋 𝑈 = (𝑦𝐻𝑥)))
5655elrab 3679 . . . . . . . . . 10 (𝑈 ∈ {𝑧𝑋 ∣ ∃𝑦𝑋 𝑧 = (𝑦𝐻𝑥)} ↔ (𝑈𝑋 ∧ ∃𝑦𝑋 𝑈 = (𝑦𝐻𝑥)))
5753, 56sylib 217 . . . . . . . . 9 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → (𝑈𝑋 ∧ ∃𝑦𝑋 𝑈 = (𝑦𝐻𝑥)))
5857simprd 496 . . . . . . . 8 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦𝑋 𝑈 = (𝑦𝐻𝑥))
59 eqcom 2738 . . . . . . . . 9 ((𝑦𝐻𝑥) = 𝑈𝑈 = (𝑦𝐻𝑥))
6059rexbii 3093 . . . . . . . 8 (∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈 ↔ ∃𝑦𝑋 𝑈 = (𝑦𝐻𝑥))
6158, 60sylibr 233 . . . . . . 7 (((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) ∧ 𝑥 ∈ (𝑋 ∖ {𝑍})) → ∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈)
6261ralrimiva 3145 . . . . . 6 ((𝐾 ∈ CRingOps ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈)
63623adant2 1131 . . . . 5 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈)
6414, 15, 63jca32 516 . . . 4 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → (𝐾 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈)))
653, 4, 6, 5, 7isdrngo3 36632 . . . 4 (𝐾 ∈ DivRingOps ↔ (𝐾 ∈ RingOps ∧ (𝑈𝑍 ∧ ∀𝑥 ∈ (𝑋 ∖ {𝑍})∃𝑦𝑋 (𝑦𝐻𝑥) = 𝑈)))
6664, 65sylibr 233 . . 3 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ DivRingOps)
67 simp1 1136 . . 3 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ CRingOps)
68 isfld2 36678 . . 3 (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps))
6966, 67, 68sylanbrc 583 . 2 ((𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}) → 𝐾 ∈ Fld)
7012, 69impbii 208 1 (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2939  wral 3060  wrex 3069  {crab 3431  cdif 3941  wss 3944  {csn 4622  {cpr 4624  ran crn 5670  cfv 6532  (class class class)co 7393  1st c1st 7955  2nd c2nd 7956  GIdcgi 29606  RingOpscrngo 36567  DivRingOpscdrng 36621  Fldcfld 36664  CRingOpsccring 36666  Idlcidl 36680   IdlGen cigen 36732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-1st 7957  df-2nd 7958  df-1o 8448  df-en 8923  df-grpo 29609  df-gid 29610  df-ginv 29611  df-ablo 29661  df-ass 36516  df-exid 36518  df-mgmOLD 36522  df-sgrOLD 36534  df-mndo 36540  df-rngo 36568  df-drngo 36622  df-com2 36663  df-fld 36665  df-crngo 36667  df-idl 36683  df-igen 36733
This theorem is referenced by:  isfldidl2  36742
  Copyright terms: Public domain W3C validator