Definition df-nmo 24645

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 24642	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24514	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1539	. . . . 5 class 𝑠
7	3	cv 1539	. . . . 5 class 𝑡
8		cghm 19193	. . . . 5 class GrpHom
9	6, 7, 8	co 7403	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1539	. . . . . . . . . 10 class 𝑥
12	5	cv 1539	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6530	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24513	. . . . . . . . . 10 class norm
15	7, 14	cfv 6530	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6530	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1539	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6530	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6530	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11132	. . . . . . . . 9 class ·
22	18, 20, 21	co 7403	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11268	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5119	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17226	. . . . . . . 8 class Base
26	6, 25	cfv 6530	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3051	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11127	. . . . . . 7 class 0
29		cpnf 11264	. . . . . . 7 class +∞
30		cico 13362	. . . . . . 7 class [,)
31	28, 29, 30	co 7403	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3415	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11266	. . . . 5 class ℝ*
34		clt 11267	. . . . 5 class <
35	32, 33, 34	cinf 9451	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5201	. . 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 1540	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24648  nmofval  24651