Metamath Proof Explorer

Theorem bddnghm

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

Ref Expression
Hypothesis nmofval.1 
|- N = ( S normOp T )
Assertion bddnghm 
|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( A e. RR /\ ( N ` F ) <_ A ) ) -> F e. ( S NGHom T ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 1 nmocl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
3 1 nmoge0 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
4 2 3 jca 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) )
5 xrrege0 
 |-  ( ( ( ( N ` F ) e. RR* /\ A e. RR ) /\ ( 0 <_ ( N ` F ) /\ ( N ` F ) <_ A ) ) -> ( N ` F ) e. RR )
6 5 an4s 
 |-  ( ( ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) /\ ( A e. RR /\ ( N ` F ) <_ A ) ) -> ( N ` F ) e. RR )
7 4 6 sylan 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( A e. RR /\ ( N ` F ) <_ A ) ) -> ( N ` F ) e. RR )
8 1 isnghm2 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
9 8 adantr 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( A e. RR /\ ( N ` F ) <_ A ) ) -> ( F e. ( S NGHom T ) <-> ( N ` F ) e. RR ) )
10 7 9 mpbird 
 |-  ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ ( A e. RR /\ ( N ` F ) <_ A ) ) -> F e. ( S NGHom T ) )