Metamath Proof Explorer

Theorem isnghm3

Description: A normed group homomorphism is a group homomorphism with bounded norm. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Hypothesis nmofval.1 
|- N = ( S normOp T )
Assertion isnghm3 
|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) < +oo ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 1 isnghm2 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
3 1 nmocl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
4 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
5 ge0gtmnf 
 |-  ( ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) -> -oo < ( N ` F ) )
6 3 4 5 syl2anc 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> -oo < ( N ` F ) )
7 xrrebnd 
 |-  ( ( N ` F ) e. RR* -> ( ( N ` F ) e. RR <-> ( -oo < ( N ` F ) /\ ( N ` F ) < +oo ) ) )
8 7 baibd 
 |-  ( ( ( N ` F ) e. RR* /\ -oo < ( N ` F ) ) -> ( ( N ` F ) e. RR <-> ( N ` F ) < +oo ) )
9 3 6 8 syl2anc 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) e. RR <-> ( N ` F ) < +oo ) )
10 2 9 bitrd 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) < +oo ) )