rrextdrg

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

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

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
3		eqid	$⊢ ℤMod (R) = ℤMod (R)$
4	1 2 3	isrrext	$⊢ R \in ℝExt \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land (ℤMod (R) \in NrmMod \land chr (R) = 0) \land (R \in CUnifSp \land UnifSt (R) = metUnif ({dist (R) ↾}_{({Base}_{R} \times {Base}_{R})})))$
5	4	simp1bi	$⊢ R \in ℝExt \to (R \in NrmRing \land R \in DivRing)$
6	5	simprd	$⊢ R \in ℝExt \to R \in DivRing$

Metamath Proof Explorer