Definition df-nmo 24744

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 24741	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24605	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1535	. . . . 5 class 𝑠
7	3	cv 1535	. . . . 5 class 𝑡
8		cghm 19242	. . . . 5 class GrpHom
9	6, 7, 8	co 7430	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1535	. . . . . . . . . 10 class 𝑥
12	5	cv 1535	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6562	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24604	. . . . . . . . . 10 class norm
15	7, 14	cfv 6562	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6562	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1535	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6562	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6562	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11157	. . . . . . . . 9 class ·
22	18, 20, 21	co 7430	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11293	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5147	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17244	. . . . . . . 8 class Base
26	6, 25	cfv 6562	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3058	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11152	. . . . . . 7 class 0
29		cpnf 11289	. . . . . . 7 class +∞
30		cico 13385	. . . . . . 7 class [,)
31	28, 29, 30	co 7430	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3432	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11291	. . . . 5 class ℝ*
34		clt 11292	. . . . 5 class <
35	32, 33, 34	cinf 9478	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5230	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7432	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1536	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24747  nmofval  24750