MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfld Structured version   Visualization version   GIF version

Theorem isfld 20049
Description: A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
Assertion
Ref Expression
isfld (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))

Proof of Theorem isfld
StepHypRef Expression
1 df-field 20043 . 2 Field = (DivRing ∩ CRing)
21elin2 4137 1 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wcel 2104  CRingccrg 19833  DivRingcdr 20040  Fieldcfield 20041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-field 20043
This theorem is referenced by:  fldpropd  20068  primefld  20122  rng1nfld  20598  fldidom  20625  fldidomOLD  20626  fiidomfld  20629  refld  20873  recrng  20875  frlmphllem  21036  frlmphl  21037  recvs  24358  rrxcph  24605  rrx0  24610  ply1pid  25393  lgseisenlem3  26574  lgseisenlem4  26575  ofldlt1  31561  ofldchr  31562  subofld  31564  isarchiofld  31565  reofld  31593  rearchi  31595  srafldlvec  31725  rgmoddim  31742  ccfldextrr  31772  fldextsralvec  31779  extdgcl  31780  extdggt0  31781  fldextid  31783  extdgmul  31785  extdg1id  31787  ccfldsrarelvec  31790  qqhrhm  31988  matunitlindflem1  35821  matunitlindflem2  35822  matunitlindf  35823  fldcrngd  40450  prjcrv0  40665  fldcat  45884  fldcatALTV  45902
  Copyright terms: Public domain W3C validator