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 ) ) |
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 ) ) |