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

Theorem rrextnlm 31318
Description: The norm of an extension of is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018.)
Hypothesis
Ref Expression
rrextnlm.z 𝑍 = (ℤMod‘𝑅)
Assertion
Ref Expression
rrextnlm (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)

Proof of Theorem rrextnlm
StepHypRef Expression
1 eqid 2822 . . . 4 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2822 . . . 4 ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3 rrextnlm.z . . . 4 𝑍 = (ℤMod‘𝑅)
41, 2, 3isrrext 31315 . . 3 (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
54simp2bi 1143 . 2 (𝑅 ∈ ℝExt → (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0))
65simpld 498 1 (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2114   × cxp 5530  cres 5534  cfv 6334  0cc0 10526  Basecbs 16474  distcds 16565  DivRingcdr 19493  metUnifcmetu 20080  ℤModczlm 20192  chrcchr 20193  UnifStcuss 22857  CUnifSpccusp 22901  NrmRingcnrg 23184  NrmModcnlm 23185   ℝExt crrext 31309
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-xp 5538  df-res 5544  df-iota 6293  df-fv 6342  df-rrext 31314
This theorem is referenced by:  rrhfe  31327  rrhcne  31328  rrhqima  31329  sitgclg  31674
  Copyright terms: Public domain W3C validator