Theorem rrextdrg 34003

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

Assertion

Ref	Expression
rrextdrg	⊢ (𝑅 ∈ ℝExt → 𝑅 ∈ DivRing)

Proof of Theorem rrextdrg

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   × cxp 5683   ↾ cres 5687  ‘cfv 6561  0cc0 11155  Basecbs 17247  distcds 17306  DivRingcdr 20729  metUnifcmetu 21355  ℤModczlm 21511  chrcchr 21512  UnifStcuss 24262  CUnifSpccusp 24306  NrmRingcnrg 24592  NrmModcnlm 24593   ℝExt crrext 33995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-res 5697  df-iota 6514  df-fv 6569  df-rrext 34000

This theorem is referenced by:  rrhfe  34013  rrhcne  34014  rrhqima  34015  rrh0  34016  sitgclg  34344