Definition df-nmo 24623

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 24620	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24492	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1540	. . . . 5 class 𝑠
7	3	cv 1540	. . . . 5 class 𝑡
8		cghm 19124	. . . . 5 class GrpHom
9	6, 7, 8	co 7346	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1540	. . . . . . . . . 10 class 𝑥
12	5	cv 1540	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6481	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24491	. . . . . . . . . 10 class norm
15	7, 14	cfv 6481	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6481	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1540	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6481	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6481	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11011	. . . . . . . . 9 class ·
22	18, 20, 21	co 7346	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11147	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5089	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17120	. . . . . . . 8 class Base
26	6, 25	cfv 6481	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3047	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11006	. . . . . . 7 class 0
29		cpnf 11143	. . . . . . 7 class +∞
30		cico 13247	. . . . . . 7 class [,)
31	28, 29, 30	co 7346	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3395	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11145	. . . . 5 class ℝ*
34		clt 11146	. . . . 5 class <
35	32, 33, 34	cinf 9325	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5170	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7348	. 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  24626  nmofval  24629