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

Theorem rrextnrg 28420
Description: An extension of  RR is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)
Assertion
Ref Expression
rrextnrg  |-  ( R  e. ℝExt  ->  R  e. NrmRing )

Proof of Theorem rrextnrg
StepHypRef Expression
1 eqid 2402 . . . 4  |-  ( Base `  R )  =  (
Base `  R )
2 eqid 2402 . . . 4  |-  ( (
dist `  R )  |`  ( ( Base `  R
)  X.  ( Base `  R ) ) )  =  ( ( dist `  R )  |`  (
( Base `  R )  X.  ( Base `  R
) ) )
3 eqid 2402 . . . 4  |-  ( ZMod
`  R )  =  ( ZMod `  R
)
41, 2, 3isrrext 28419 . . 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 1012 . 2  |-  ( R  e. ℝExt  ->  ( R  e. NrmRing  /\  R  e.  DivRing ) )
65simpld 457 1  |-  ( R  e. ℝExt  ->  R  e. NrmRing )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842    X. cxp 4820    |` cres 4824   ` cfv 5568   0cc0 9521   Basecbs 14839   distcds 14916   DivRingcdr 17714  metUnifcmetu 18728   ZModczlm 18836  chrcchr 18837  UnifStcuss 21046  CUnifSpccusp 21090  NrmRingcnrg 21390  NrmModcnlm 21391   ℝExt crrext 28413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-opab 4453  df-xp 4828  df-res 4834  df-iota 5532  df-fv 5576  df-rrext 28418
This theorem is referenced by:  rrexttps  28425  rrexthaus  28426  rrhfe  28430  rrhcne  28431  sitgclg  28776
  Copyright terms: Public domain W3C validator