Definition df-nmo 25020

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 25017	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24889	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1569	. . . . 5 class 𝑠
7	3	cv 1569	. . . . 5 class 𝑡
8		cghm 19420	. . . . 5 class GrpHom
9	6, 7, 8	co 7418	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1569	. . . . . . . . . 10 class 𝑥
12	5	cv 1569	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6537	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24888	. . . . . . . . . 10 class norm
15	7, 14	cfv 6537	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6537	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1569	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6537	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6537	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11198	. . . . . . . . 9 class ·
22	18, 20, 21	co 7418	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11337	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5103	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17380	. . . . . . . 8 class Base
26	6, 25	cfv 6537	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3077	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11193	. . . . . . 7 class 0
29		cpnf 11333	. . . . . . 7 class +∞
30		cico 13471	. . . . . . 7 class [,)
31	28, 29, 30	co 7418	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3413	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11335	. . . . 5 class ℝ*
34		clt 11336	. . . . 5 class <
35	32, 33, 34	cinf 9426	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5186	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7420	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1570	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is used by:  nmoffn  25023  nmofval  25026