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=sNrmGrp,tNrmGrpsnormOpt-1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnghm classNGHom
1 vs setvars
2 cngp classNrmGrp
3 vt setvart
4 1 cv setvars
5 cnmo classnormOp
6 3 cv setvart
7 4 6 5 co classsnormOpt
8 7 ccnv classsnormOpt-1
9 cr class
10 8 9 cima classsnormOpt-1
11 1 3 2 2 10 cmpo classsNrmGrp,tNrmGrpsnormOpt-1
12 0 11 wceq wffNGHom=sNrmGrp,tNrmGrpsnormOpt-1