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

Definition df-nmhm 18744
 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 such that (Contributed by Mario Carneiro, 18-Oct-2015.)
Assertion
Ref Expression
df-nmhm NMHom NrmMod NrmMod LMHom NGHom
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-nmhm
StepHypRef Expression
1 cnmhm 18741 . 2 NMHom
2 vs . . 3
3 vt . . 3
4 cnlm 18628 . . 3 NrmMod
52cv 1651 . . . . 5
63cv 1651 . . . . 5
7 clmhm 16095 . . . . 5 LMHom
85, 6, 7co 6081 . . . 4 LMHom
9 cnghm 18740 . . . . 5 NGHom
105, 6, 9co 6081 . . . 4 NGHom
118, 10cin 3319 . . 3 LMHom NGHom
122, 3, 4, 4, 11cmpt2 6083 . 2 NrmMod NrmMod LMHom NGHom
131, 12wceq 1652 1 NMHom NrmMod NrmMod LMHom NGHom
 Colors of variables: wff set class This definition is referenced by:  reldmnmhm  18747  isnmhm  18780
 Copyright terms: Public domain W3C validator