Definition df-nmo 24596

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 24593	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24465	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1539	. . . . 5 class 𝑠
7	3	cv 1539	. . . . 5 class 𝑡
8		cghm 19144	. . . . 5 class GrpHom
9	6, 7, 8	co 7387	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1539	. . . . . . . . . 10 class 𝑥
12	5	cv 1539	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6511	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24464	. . . . . . . . . 10 class norm
15	7, 14	cfv 6511	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6511	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1539	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6511	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6511	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11073	. . . . . . . . 9 class ·
22	18, 20, 21	co 7387	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11209	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5107	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17179	. . . . . . . 8 class Base
26	6, 25	cfv 6511	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3044	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11068	. . . . . . 7 class 0
29		cpnf 11205	. . . . . . 7 class +∞
30		cico 13308	. . . . . . 7 class [,)
31	28, 29, 30	co 7387	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3405	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11207	. . . . 5 class ℝ*
34		clt 11208	. . . . 5 class <
35	32, 33, 34	cinf 9392	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5188	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7389	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1540	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24599  nmofval  24602