Definition df-nmhm 22324

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

Step	Hyp	Ref	Expression
1		cnmhm 22321	. 2 class NMHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cnlm 22195	. . 3 class NrmMod
5	2	cv 1474	. . . . 5 class 𝑠
6	3	cv 1474	. . . . 5 class 𝑡
7		clmhm 18840	. . . . 5 class LMHom
8	5, 6, 7	co 6549	. . . 4 class (𝑠 LMHom 𝑡)
9		cnghm 22320	. . . . 5 class NGHom
10	5, 6, 9	co 6549	. . . 4 class (𝑠 NGHom 𝑡)
11	8, 10	cin 3539	. . 3 class ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡))
12	2, 3, 4, 4, 11	cmpt2 6551	. 2 class (𝑠 ∈ NrmMod, 𝑡 ∈ NrmMod ↦ ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡)))
13	1, 12	wceq 1475	1 wff NMHom = (𝑠 ∈ NrmMod, 𝑡 ∈ NrmMod ↦ ((𝑠 LMHom 𝑡) ∩ (𝑠 NGHom 𝑡)))

This definition is referenced by:  reldmnmhm  22327  isnmhm  22360