Definition df-nmo 24224

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 24221	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24085	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1540	. . . . 5 class 𝑠
7	3	cv 1540	. . . . 5 class 𝑡
8		cghm 19088	. . . . 5 class GrpHom
9	6, 7, 8	co 7408	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1540	. . . . . . . . . 10 class 𝑥
12	5	cv 1540	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6543	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24084	. . . . . . . . . 10 class norm
15	7, 14	cfv 6543	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6543	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1540	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6543	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6543	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11114	. . . . . . . . 9 class ·
22	18, 20, 21	co 7408	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11248	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5148	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17143	. . . . . . . 8 class Base
26	6, 25	cfv 6543	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3061	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11109	. . . . . . 7 class 0
29		cpnf 11244	. . . . . . 7 class +∞
30		cico 13325	. . . . . . 7 class [,)
31	28, 29, 30	co 7408	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3432	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11246	. . . . 5 class ℝ*
34		clt 11247	. . . . 5 class <
35	32, 33, 34	cinf 9435	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5231	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7410	. 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  24227  nmofval  24230