Definition df-nmhm 22514

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.)

Assertion

Ref	Expression
df-nmhm	|- NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) )

Distinct variable group:   t, s

Detailed syntax breakdown of Definition df-nmhm

Step	Hyp	Ref	Expression
1		cnmhm 22511	. 2 class NMHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cnlm 22385	. . 3 class NrmMod
5	2	cv 1482	. . . . 5 class s
6	3	cv 1482	. . . . 5 class t
7		clmhm 19019	. . . . 5 class LMHom
8	5, 6, 7	co 6650	. . . 4 class ( s LMHom t )
9		cnghm 22510	. . . . 5 class NGHom
10	5, 6, 9	co 6650	. . . 4 class ( s NGHom t )
11	8, 10	cin 3573	. . 3 class ( ( s LMHom t ) i^i ( s NGHom t ) )
12	2, 3, 4, 4, 11	cmpt2 6652	. 2 class ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) )
13	1, 12	wceq 1483	1 wff NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) )

This definition is referenced by:  reldmnmhm  22517  isnmhm  22550