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 31949
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 2740 . . . 4 (Base‘𝑅) = (Base‘𝑅)
2 eqid 2740 . . . 4 ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3 rrextnlm.z . . . 4 𝑍 = (ℤMod‘𝑅)
41, 2, 3isrrext 31946 . . 3 (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
54simp2bi 1145 . 2 (𝑅 ∈ ℝExt → (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0))
65simpld 495 1 (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1542  wcel 2110   × cxp 5588  cres 5592  cfv 6432  0cc0 10872  Basecbs 16910  distcds 16969  DivRingcdr 19989  metUnifcmetu 20586  ℤModczlm 20700  chrcchr 20701  UnifStcuss 23403  CUnifSpccusp 23447  NrmRingcnrg 23733  NrmModcnlm 23734   ℝExt crrext 31940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5596  df-res 5602  df-iota 6390  df-fv 6440  df-rrext 31945
This theorem is referenced by:  rrhfe  31958  rrhcne  31959  rrhqima  31960  sitgclg  32305
  Copyright terms: Public domain W3C validator