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