Definition df-nmo 24206

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 24203	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24067	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1541	. . . . 5 class 𝑠
7	3	cv 1541	. . . . 5 class 𝑡
8		cghm 19082	. . . . 5 class GrpHom
9	6, 7, 8	co 7403	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1541	. . . . . . . . . 10 class 𝑥
12	5	cv 1541	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6539	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24066	. . . . . . . . . 10 class norm
15	7, 14	cfv 6539	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6539	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1541	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6539	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6539	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11110	. . . . . . . . 9 class ·
22	18, 20, 21	co 7403	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11244	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5146	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17139	. . . . . . . 8 class Base
26	6, 25	cfv 6539	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3062	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11105	. . . . . . 7 class 0
29		cpnf 11240	. . . . . . 7 class +∞
30		cico 13321	. . . . . . 7 class [,)
31	28, 29, 30	co 7403	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3433	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11242	. . . . 5 class ℝ*
34		clt 11243	. . . . 5 class <
35	32, 33, 34	cinf 9431	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5229	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7405	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1542	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24209  nmofval  24212