Definition df-nmo 24765

Description: Define the norm of an operator between two normed groups (usually vector spaces). This definition produces an operator norm function for each pair of groups ⟨𝑠, 𝑡⟩. Equivalent to the definition of linear operator norm in [AkhiezerGlazman] p. 39. (Contributed by Mario Carneiro, 18-Oct-2015.) (Revised by AV, 25-Sep-2020.)

Assertion

Ref	Expression
df-nmo	⊢ normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

Distinct variable group:   𝑓,𝑟,𝑠,𝑡,𝑥

Detailed syntax breakdown of Definition df-nmo

Step	Hyp	Ref	Expression
1		cnmo 24762	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24634	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1559	. . . . 5 class 𝑠
7	3	cv 1559	. . . . 5 class 𝑡
8		cghm 19253	. . . . 5 class GrpHom
9	6, 7, 8	co 7396	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1559	. . . . . . . . . 10 class 𝑥
12	5	cv 1559	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6521	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24633	. . . . . . . . . 10 class norm
15	7, 14	cfv 6521	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6521	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1559	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6521	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6521	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11078	. . . . . . . . 9 class ·
22	18, 20, 21	co 7396	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11217	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5100	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17245	. . . . . . . 8 class Base
26	6, 25	cfv 6521	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3076	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11073	. . . . . . 7 class 0
29		cpnf 11213	. . . . . . 7 class +∞
30		cico 13351	. . . . . . 7 class [,)
31	28, 29, 30	co 7396	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3414	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11215	. . . . 5 class ℝ*
34		clt 11216	. . . . 5 class <
35	32, 33, 34	cinf 9387	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5181	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7398	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1560	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24768  nmofval  24771