Theorem rrextdrg

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

	Ref	Expression
Assertion	rrextdrg	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
2		eqid	$$⊢{\mathrm{dist}\left(R\right)\upharpoonright }_{\left({\mathrm{Base}}_R\times {\mathrm{Base}}_R\right)}={\mathrm{dist}\left(R\right)\upharpoonright }_{\left({\mathrm{Base}}_R\times {\mathrm{Base}}_R\right)}$$
3		eqid	$$⊢\mathrm{\mathbb{Z}Mod}\left(R\right)=\mathrm{\mathbb{Z}Mod}\left(R\right)$$
4	1 2 3	isrrext	$$⊢R\in \mathrm{ℝExt}\leftrightarrow \left(\left(R\in \mathrm{NrmRing}\wedge R\in \mathrm{DivRing}\right)\wedge \left(\mathrm{\mathbb{Z}Mod}\left(R\right)\in \mathrm{NrmMod}\wedge \mathrm{chr}\left(R\right)=0\right)\wedge \left(R\in \mathrm{CUnifSp}\wedge \mathrm{UnifSt}\left(R\right)=\mathrm{metUnif}\left({\mathrm{dist}\left(R\right)\upharpoonright }_{\left({\mathrm{Base}}_R\times {\mathrm{Base}}_R\right)}\right)\right)\right)$$
5	4	simp1bi	$$⊢R\in \mathrm{ℝExt}\to \left(R\in \mathrm{NrmRing}\wedge R\in \mathrm{DivRing}\right)$$
6	5	simprd	$$⊢R\in \mathrm{ℝExt}\to R\in \mathrm{DivRing}$$