MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nghm Unicode version

Definition df-nghm 18218
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.)
Assertion
Ref Expression
df-nghm  |- NGHom  =  ( s  e. NrmGrp ,  t  e. NrmGrp  |->  ( `' ( s
normOp t ) " RR ) )
Distinct variable group:    t, s

Detailed syntax breakdown of Definition df-nghm
StepHypRef Expression
1 cnghm 18215 . 2  class NGHom
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cngp 18100 . . 3  class NrmGrp
52cv 1622 . . . . . 6  class  s
63cv 1622 . . . . . 6  class  t
7 cnmo 18214 . . . . . 6  class  normOp
85, 6, 7co 5858 . . . . 5  class  ( s
normOp t )
98ccnv 4688 . . . 4  class  `' ( s normOp t )
10 cr 8736 . . . 4  class  RR
119, 10cima 4692 . . 3  class  ( `' ( s normOp t )
" RR )
122, 3, 4, 4, 11cmpt2 5860 . 2  class  ( s  e. NrmGrp ,  t  e. NrmGrp  |->  ( `' ( s normOp t ) " RR ) )
131, 12wceq 1623 1  wff NGHom  =  ( s  e. NrmGrp ,  t  e. NrmGrp  |->  ( `' ( s
normOp t ) " RR ) )
Colors of variables: wff set class
This definition is referenced by:  reldmnghm  18221  nghmfval  18231
  Copyright terms: Public domain W3C validator