Definition df-nmo 23317

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 23314	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 23187	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1536	. . . . 5 class 𝑠
7	3	cv 1536	. . . . 5 class 𝑡
8		cghm 18355	. . . . 5 class GrpHom
9	6, 7, 8	co 7156	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1536	. . . . . . . . . 10 class 𝑥
12	5	cv 1536	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6355	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 23186	. . . . . . . . . 10 class norm
15	7, 14	cfv 6355	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6355	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1536	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6355	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6355	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 10542	. . . . . . . . 9 class ·
22	18, 20, 21	co 7156	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 10676	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5066	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 16483	. . . . . . . 8 class Base
26	6, 25	cfv 6355	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3138	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 10537	. . . . . . 7 class 0
29		cpnf 10672	. . . . . . 7 class +∞
30		cico 12741	. . . . . . 7 class [,)
31	28, 29, 30	co 7156	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3142	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 10674	. . . . 5 class ℝ*
34		clt 10675	. . . . 5 class <
35	32, 33, 34	cinf 8905	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5146	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7158	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1537	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  23320  nmofval  23323