Definition df-nmo 24686

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 24683	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24555	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1541	. . . . 5 class 𝑠
7	3	cv 1541	. . . . 5 class 𝑡
8		cghm 19181	. . . . 5 class GrpHom
9	6, 7, 8	co 7361	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1541	. . . . . . . . . 10 class 𝑥
12	5	cv 1541	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6493	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24554	. . . . . . . . . 10 class norm
15	7, 14	cfv 6493	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6493	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1541	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6493	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6493	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11037	. . . . . . . . 9 class ·
22	18, 20, 21	co 7361	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11174	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5086	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17173	. . . . . . . 8 class Base
26	6, 25	cfv 6493	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3052	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11032	. . . . . . 7 class 0
29		cpnf 11170	. . . . . . 7 class +∞
30		cico 13294	. . . . . . 7 class [,)
31	28, 29, 30	co 7361	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3390	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11172	. . . . 5 class ℝ*
34		clt 11173	. . . . 5 class <
35	32, 33, 34	cinf 9348	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5167	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7363	. 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  24689  nmofval  24692