Metamath Proof Explorer


Definition df-nghm

Description: Define the set of normed group homomorphisms between two normed groups. A normed group homomorphism is a group homomorphism which additionally bounds the increase of norm by a fixed real operator. In vector spaces these are also known as bounded linear operators. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Assertion df-nghm
|- NGHom = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnghm
 |-  NGHom
1 vs
 |-  s
2 cngp
 |-  NrmGrp
3 vt
 |-  t
4 1 cv
 |-  s
5 cnmo
 |-  normOp
6 3 cv
 |-  t
7 4 6 5 co
 |-  ( s normOp t )
8 7 ccnv
 |-  `' ( s normOp t )
9 cr
 |-  RR
10 8 9 cima
 |-  ( `' ( s normOp t ) " RR )
11 1 3 2 2 10 cmpo
 |-  ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )
12 0 11 wceq
 |-  NGHom = ( s e. NrmGrp , t e. NrmGrp |-> ( `' ( s normOp t ) " RR ) )