Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rrextdrg Structured version   Unicode version

Theorem rrextdrg 27607
Description: An extension of  RR is a division ring. (Contributed by Thierry Arnoux, 2-May-2018.)
Assertion
Ref Expression
rrextdrg  |-  ( R  e. ℝExt  ->  R  e.  DivRing )

Proof of Theorem rrextdrg
StepHypRef Expression
1 eqid 2462 . . . 4  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2462 . . . 4  |-  ( (
dist `  R )  |`  ( ( Base `  R
)  X.  ( Base `  R ) ) )  =  ( ( dist `  R )  |`  (
( Base `  R )  X.  ( Base `  R
) ) )
3 eqid 2462 . . . 4  |-  ( ZMod
`  R )  =  ( ZMod `  R
)
41, 2, 3isrrext 27605 . . 3  |-  ( R  e. ℝExt 
<->  ( ( R  e. NrmRing  /\  R  e.  DivRing )  /\  ( ( ZMod `  R )  e. NrmMod  /\  (chr `  R )  =  0 )  /\  ( R  e. CUnifSp  /\  (UnifSt `  R
)  =  (metUnif `  (
( dist `  R )  |`  ( ( Base `  R
)  X.  ( Base `  R ) ) ) ) ) ) )
54simp1bi 1006 . 2  |-  ( R  e. ℝExt  ->  ( R  e. NrmRing  /\  R  e.  DivRing ) )
65simprd 463 1  |-  ( R  e. ℝExt  ->  R  e.  DivRing )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1374    e. wcel 1762    X. cxp 4992    |` cres 4996   ` cfv 5581   0cc0 9483   Basecbs 14481   distcds 14555   DivRingcdr 17174  metUnifcmetu 18176   ZModczlm 18300  chrcchr 18301  UnifStcuss 20486  CUnifSpccusp 20530  NrmRingcnrg 20830  NrmModcnlm 20831   ℝExt crrext 27599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-opab 4501  df-xp 5000  df-res 5006  df-iota 5544  df-fv 5589  df-rrext 27604
This theorem is referenced by:  rrhfe  27616  rrhcne  27617  sitgclg  27912
  Copyright terms: Public domain W3C validator