Definition df-nmo 23872

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 23869	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 23733	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . 5 class 𝑠
7	3	cv 1538	. . . . 5 class 𝑡
8		cghm 18831	. . . . 5 class GrpHom
9	6, 7, 8	co 7275	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1538	. . . . . . . . . 10 class 𝑥
12	5	cv 1538	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6433	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 23732	. . . . . . . . . 10 class norm
15	7, 14	cfv 6433	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6433	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1538	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6433	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6433	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 10876	. . . . . . . . 9 class ·
22	18, 20, 21	co 7275	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11010	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5074	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 16912	. . . . . . . 8 class Base
26	6, 25	cfv 6433	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3064	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 10871	. . . . . . 7 class 0
29		cpnf 11006	. . . . . . 7 class +∞
30		cico 13081	. . . . . . 7 class [,)
31	28, 29, 30	co 7275	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3068	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11008	. . . . 5 class ℝ*
34		clt 11009	. . . . 5 class <
35	32, 33, 34	cinf 9200	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5157	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7277	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1539	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  23875  nmofval  23878