df-nmhm

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 \in NrmMod, t \in NrmMod ⟼ (s LMHom t) \cap (s NGHom t))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmhm	$class NMHom$
1		vs	$setvar s$
2		cnlm	$class NrmMod$
3		vt	$setvar t$
4	1	cv	$setvar s$
5		clmhm	$class LMHom$
6	3	cv	$setvar t$
7	4 6 5	co	$class (s LMHom t)$
8		cnghm	$class NGHom$
9	4 6 8	co	$class (s NGHom t)$
10	7 9	cin	$class ((s LMHom t) \cap (s NGHom t))$
11	1 3 2 2 10	cmpo	$class (s \in NrmMod, t \in NrmMod ⟼ (s LMHom t) \cap (s NGHom t))$
12	0 11	wceq	$wff NMHom = (s \in NrmMod, t \in NrmMod ⟼ (s LMHom t) \cap (s NGHom t))$

Metamath Proof Explorer

Definition df-nmhm

Detailed syntax breakdown