Definition df-nmo 24652

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 24649	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24521	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1540	. . . . 5 class 𝑠
7	3	cv 1540	. . . . 5 class 𝑡
8		cghm 19141	. . . . 5 class GrpHom
9	6, 7, 8	co 7358	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1540	. . . . . . . . . 10 class 𝑥
12	5	cv 1540	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6492	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24520	. . . . . . . . . 10 class norm
15	7, 14	cfv 6492	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6492	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1540	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6492	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6492	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11031	. . . . . . . . 9 class ·
22	18, 20, 21	co 7358	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11167	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5098	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17136	. . . . . . . 8 class Base
26	6, 25	cfv 6492	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3051	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11026	. . . . . . 7 class 0
29		cpnf 11163	. . . . . . 7 class +∞
30		cico 13263	. . . . . . 7 class [,)
31	28, 29, 30	co 7358	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3399	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11165	. . . . 5 class ℝ*
34		clt 11166	. . . . 5 class <
35	32, 33, 34	cinf 9344	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5179	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7360	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1541	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24655  nmofval  24658