Theorem rrextnlm 33637

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

Step	Hyp	Ref	Expression
1		eqid 2728	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2728	. . . 4 ⊢ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3		rrextnlm.z	. . . 4 ⊢ 𝑍 = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 33634	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
5	4	simp2bi 1143	. 2 ⊢ (𝑅 ∈ ℝExt → (𝑍 ∈ NrmMod ∧ (chr‘𝑅) = 0))
6	5	simpld 493	1 ⊢ (𝑅 ∈ ℝExt → 𝑍 ∈ NrmMod)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098   × cxp 5680   ↾ cres 5684  ‘cfv 6553  0cc0 11146  Basecbs 17187  distcds 17249  DivRingcdr 20631  metUnifcmetu 21277  ℤModczlm 21433  chrcchr 21434  UnifStcuss 24178  CUnifSpccusp 24222  NrmRingcnrg 24508  NrmModcnlm 24509   ℝExt crrext 33628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-xp 5688  df-res 5694  df-iota 6505  df-fv 6561  df-rrext 33633

This theorem is referenced by:  rrhfe  33646  rrhcne  33647  rrhqima  33648  sitgclg  33995