Definition df-nmo 24572

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 24569	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24441	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1539	. . . . 5 class 𝑠
7	3	cv 1539	. . . . 5 class 𝑡
8		cghm 19120	. . . . 5 class GrpHom
9	6, 7, 8	co 7369	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1539	. . . . . . . . . 10 class 𝑥
12	5	cv 1539	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6499	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24440	. . . . . . . . . 10 class norm
15	7, 14	cfv 6499	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6499	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1539	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6499	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6499	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11049	. . . . . . . . 9 class ·
22	18, 20, 21	co 7369	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11185	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5102	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17155	. . . . . . . 8 class Base
26	6, 25	cfv 6499	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3044	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11044	. . . . . . 7 class 0
29		cpnf 11181	. . . . . . 7 class +∞
30		cico 13284	. . . . . . 7 class [,)
31	28, 29, 30	co 7369	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3402	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11183	. . . . 5 class ℝ*
34		clt 11184	. . . . 5 class <
35	32, 33, 34	cinf 9368	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5183	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7371	. 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  24575  nmofval  24578