Metamath Proof Explorer

Theorem 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 = ( ZMod ` R )
Assertion rrextnlm 
|- ( R e. RRExt -> Z e. NrmMod )

Proof

Step Hyp Ref Expression
1 rrextnlm.z 
 |-  Z = ( ZMod ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) = ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) )
4 2 3 1 isrrext 
 |-  ( R e. RRExt <-> ( ( R e. NrmRing /\ R e. DivRing ) /\ ( Z e. NrmMod /\ ( chr ` R ) = 0 ) /\ ( R e. CUnifSp /\ ( UnifSt ` R ) = ( metUnif ` ( ( dist ` R ) |` ( ( Base ` R ) X. ( Base ` R ) ) ) ) ) ) )
5 4 simp2bi 
 |-  ( R e. RRExt -> ( Z e. NrmMod /\ ( chr ` R ) = 0 ) )
6 5 simpld 
 |-  ( R e. RRExt -> Z e. NrmMod )