Definition df-nmo 24750

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 24747	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24611	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1536	. . . . 5 class 𝑠
7	3	cv 1536	. . . . 5 class 𝑡
8		cghm 19252	. . . . 5 class GrpHom
9	6, 7, 8	co 7448	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1536	. . . . . . . . . 10 class 𝑥
12	5	cv 1536	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6573	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24610	. . . . . . . . . 10 class norm
15	7, 14	cfv 6573	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6573	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1536	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6573	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6573	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11189	. . . . . . . . 9 class ·
22	18, 20, 21	co 7448	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11325	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5166	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17258	. . . . . . . 8 class Base
26	6, 25	cfv 6573	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3067	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11184	. . . . . . 7 class 0
29		cpnf 11321	. . . . . . 7 class +∞
30		cico 13409	. . . . . . 7 class [,)
31	28, 29, 30	co 7448	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3443	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11323	. . . . 5 class ℝ*
34		clt 11324	. . . . 5 class <
35	32, 33, 34	cinf 9510	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5249	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7450	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1537	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24753  nmofval  24756