Theorem rrextnrg 34400

Description: An extension of ℝ is a normed ring. (Contributed by Thierry Arnoux, 2-May-2018.)

Assertion

Ref	Expression
rrextnrg	⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)

Proof of Theorem rrextnrg

Step	Hyp	Ref	Expression
1		eqid 2763	. . . 4 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2763	. . . 4 ⊢ ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅))) = ((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))
3		eqid 2763	. . . 4 ⊢ (ℤMod‘𝑅) = (ℤMod‘𝑅)
4	1, 2, 3	isrrext 34399	. . 3 ⊢ (𝑅 ∈ ℝExt ↔ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing) ∧ ((ℤMod‘𝑅) ∈ NrmMod ∧ (chr‘𝑅) = 0) ∧ (𝑅 ∈ CUnifSp ∧ (UnifSt‘𝑅) = (metUnif‘((dist‘𝑅) ↾ ((Base‘𝑅) × (Base‘𝑅)))))))
5	4	simp1bi 1163	. 2 ⊢ (𝑅 ∈ ℝExt → (𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing))
6	5	simpld 499	1 ⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ NrmRing)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   × cxp 5659   ↾ cres 5663  ‘cfv 6536  0cc0 11104  Basecbs 17273  distcds 17323  DivRingcdr 20836  metUnifcmetu 21522  ℤModczlm 21659  chrcchr 21660  UnifStcuss 24419  CUnifSpccusp 24462  NrmRingcnrg 24745  NrmModcnlm 24746   ℝExt crrext 34393

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-res 5673  df-iota 6492  df-fv 6544  df-rrext 34398

This theorem is used by:  rrexttps  34405  rrexthaus  34406  rrhfe  34411  rrhcne  34412  rrhqima  34413  sitgclg  34741