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

Definition df-nmhm 23314
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 23311 . 2 class NMHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cnlm 23185 . . 3 class NrmMod
52cv 1537 . . . . 5 class 𝑠
63cv 1537 . . . . 5 class 𝑡
7 clmhm 19786 . . . . 5 class LMHom
85, 6, 7co 7146 . . . 4 class (𝑠 LMHom 𝑡)
9 cnghm 23310 . . . . 5 class NGHom
105, 6, 9co 7146 . . . 4 class (𝑠 NGHom 𝑡)
118, 10cin 3918 . . 3 class ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡))
122, 3, 4, 4, 11cmpo 7148 . 2 class (𝑠 ∈ NrmMod, 𝑡 ∈ NrmMod ↦ ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡)))
131, 12wceq 1538 1 wff NMHom = (𝑠 ∈ NrmMod, 𝑡 ∈ NrmMod ↦ ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡)))
Colors of variables: wff setvar class
This definition is referenced by:  reldmnmhm  23317  isnmhm  23350
  Copyright terms: Public domain W3C validator