Definition df-nmo 22512

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 22509	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 22382	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1482	. . . . 5 class 𝑠
7	3	cv 1482	. . . . 5 class 𝑡
8		cghm 17657	. . . . 5 class GrpHom
9	6, 7, 8	co 6650	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1482	. . . . . . . . . 10 class 𝑥
12	5	cv 1482	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 5888	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 22381	. . . . . . . . . 10 class norm
15	7, 14	cfv 5888	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 5888	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1482	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 5888	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 5888	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 9941	. . . . . . . . 9 class ·
22	18, 20, 21	co 6650	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 10075	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 4653	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 15857	. . . . . . . 8 class Base
26	6, 25	cfv 5888	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 2912	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 9936	. . . . . . 7 class 0
29		cpnf 10071	. . . . . . 7 class +∞
30		cico 12177	. . . . . . 7 class [,)
31	28, 29, 30	co 6650	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 2916	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 10073	. . . . 5 class ℝ*
34		clt 10074	. . . . 5 class <
35	32, 33, 34	cinf 8347	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 4729	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpt2 6652	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1483	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  22515  nmofval  22518