rrextnlm

Description: The norm of an extension of RR is absolutely homogeneous. (Contributed by Thierry Arnoux, 2-May-2018)

		Ref	Expression
	Hypothesis	rrextnlm.z	$⊢ Z = ℤMod (R)$
	Assertion	rrextnlm	$⊢ R \in ℝExt \to Z \in NrmMod$

Step	Hyp	Ref	Expression
1		rrextnlm.z	$⊢ Z = ℤMod (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})} = {dist (R) ↾}_{({Base}_{R} \times {Base}_{R})}$
4	2 3 1	isrrext	$⊢ R \in ℝExt \leftrightarrow ((R \in NrmRing \land R \in DivRing) \land (Z \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 (Z \in NrmMod \land chr (R) = 0)$
6	5	simpld	$⊢ R \in ℝExt \to Z \in NrmMod$

Metamath Proof Explorer