Metamath Proof Explorer


Theorem rrextdrg

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

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

Proof

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