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

Theorem flddrngd 20742
Description: A field is a division ring. (Contributed by SN, 17-Jan-2025.)
Hypothesis
Ref Expression
flddrngd.1 (𝜑𝑅 ∈ Field)
Assertion
Ref Expression
flddrngd (𝜑𝑅 ∈ DivRing)

Proof of Theorem flddrngd
StepHypRef Expression
1 flddrngd.1 . 2 (𝜑𝑅 ∈ Field)
2 isfld 20741 . . 3 (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
32simplbi 497 . 2 (𝑅 ∈ Field → 𝑅 ∈ DivRing)
41, 3syl 17 1 (𝜑𝑅 ∈ DivRing)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  CRingccrg 20232  DivRingcdr 20730  Fieldcfield 20731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957  df-field 20733
This theorem is referenced by:  ply1asclunit  33600  ply1unit  33601  ply1dg1rt  33605  m1pmeq  33609  fldgenfldext  33719  evls1fldgencl  33721  fldextrspunlsplem  33724  fldextrspunfld  33727  fldextrspunlem2  33728  fldextrspundgdvdslem  33731  fldextrspundgdvds  33732  minplyirred  33755  algextdeglem2  33760  algextdeglem3  33761  algextdeglem4  33762  algextdeglem5  33763  algextdeglem7  33765  algextdeglem8  33766  rtelextdg2lem  33768  rtelextdg2  33769  aks6d1c5lem3  42139  aks6d1c5lem2  42140  aks5lem7  42202  prjcrv0  42648
  Copyright terms: Public domain W3C validator