Metamath Proof Explorer

Theorem isnghm

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 isnghm 
|- ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )

Proof

Step Hyp Ref Expression
1 nmofval.1 
 |-  N = ( S normOp T )
2 1 nghmfval 
 |-  ( S NGHom T ) = ( `' N " RR )
3 2 eleq2i 
 |-  ( F e. ( S NGHom T ) <-> F e. ( `' N " RR ) )
4 n0i 
 |-  ( F e. ( `' N " RR ) -> -. ( `' N " RR ) = (/) )
5 nmoffn 
 |-  normOp Fn ( NrmGrp X. NrmGrp )
6 5 fndmi 
 |-  dom normOp = ( NrmGrp X. NrmGrp )
7 6 ndmov 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( S normOp T ) = (/) )
8 1 7 eqtrid 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> N = (/) )
9 8 cnveqd 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> `' N = `' (/) )
10 cnv0 
 |-  `' (/) = (/)
11 9 10 eqtrdi 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> `' N = (/) )
12 11 imaeq1d 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( `' N " RR ) = ( (/) " RR ) )
13 0ima 
 |-  ( (/) " RR ) = (/)
14 12 13 eqtrdi 
 |-  ( -. ( S e. NrmGrp /\ T e. NrmGrp ) -> ( `' N " RR ) = (/) )
15 4 14 nsyl2 
 |-  ( F e. ( `' N " RR ) -> ( S e. NrmGrp /\ T e. NrmGrp ) )
16 1 nmof 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> N : ( S GrpHom T ) --> RR* )
17 ffn 
 |-  ( N : ( S GrpHom T ) --> RR* -> N Fn ( S GrpHom T ) )
18 elpreima 
 |-  ( N Fn ( S GrpHom T ) -> ( F e. ( `' N " RR ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
19 16 17 18 3syl 
 |-  ( ( S e. NrmGrp /\ T e. NrmGrp ) -> ( F e. ( `' N " RR ) <-> ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
20 15 19 biadanii 
 |-  ( F e. ( `' N " RR ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )
21 3 20 bitri 
 |-  ( F e. ( S NGHom T ) <-> ( ( S e. NrmGrp /\ T e. NrmGrp ) /\ ( F e. ( S GrpHom T ) /\ ( N ` F ) e. RR ) ) )