Definition df-nmo 23314

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 23311	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 23184	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1537	. . . . 5 class 𝑠
7	3	cv 1537	. . . . 5 class 𝑡
8		cghm 18347	. . . . 5 class GrpHom
9	6, 7, 8	co 7135	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1537	. . . . . . . . . 10 class 𝑥
12	5	cv 1537	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6324	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 23183	. . . . . . . . . 10 class norm
15	7, 14	cfv 6324	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6324	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1537	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6324	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6324	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 10531	. . . . . . . . 9 class ·
22	18, 20, 21	co 7135	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 10665	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5030	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 16475	. . . . . . . 8 class Base
26	6, 25	cfv 6324	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3106	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 10526	. . . . . . 7 class 0
29		cpnf 10661	. . . . . . 7 class +∞
30		cico 12728	. . . . . . 7 class [,)
31	28, 29, 30	co 7135	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3110	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 10663	. . . . 5 class ℝ*
34		clt 10664	. . . . 5 class <
35	32, 33, 34	cinf 8889	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5110	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7137	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1538	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  23317  nmofval  23320