Description: Define a normed module homomorphism, also known as a bounded linear operator. This is a module homomorphism (a linear function) such that the operator norm is finite, or equivalently there is a constant c such that... (Contributed by Mario Carneiro, 18-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-nmhm | |- NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cnmhm | |- NMHom |
|
| 1 | vs | |- s |
|
| 2 | cnlm | |- NrmMod |
|
| 3 | vt | |- t |
|
| 4 | 1 | cv | |- s |
| 5 | clmhm | |- LMHom |
|
| 6 | 3 | cv | |- t |
| 7 | 4 6 5 | co | |- ( s LMHom t ) |
| 8 | cnghm | |- NGHom |
|
| 9 | 4 6 8 | co | |- ( s NGHom t ) |
| 10 | 7 9 | cin | |- ( ( s LMHom t ) i^i ( s NGHom t ) ) |
| 11 | 1 3 2 2 10 | cmpo | |- ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) ) |
| 12 | 0 11 | wceq | |- NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) ) |