rrextchr

Description: The ring characteristic of an extension of RR is zero. (Contributed by Thierry Arnoux, 2-May-2018)

		Ref	Expression
	Assertion	rrextchr	$⊢ R \in ℝExt \to chr (R) = 0$

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	simp2bi	$⊢ R \in ℝExt \to (ℤMod (R) \in NrmMod \land chr (R) = 0)$
6	5	simprd	$⊢ R \in ℝExt \to chr (R) = 0$

Metamath Proof Explorer