Definition df-nmo 24445

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 24442	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24306	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . 5 class 𝑠
7	3	cv 1538	. . . . 5 class 𝑡
8		cghm 19127	. . . . 5 class GrpHom
9	6, 7, 8	co 7411	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1538	. . . . . . . . . 10 class 𝑥
12	5	cv 1538	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6542	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24305	. . . . . . . . . 10 class norm
15	7, 14	cfv 6542	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6542	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1538	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6542	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6542	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11117	. . . . . . . . 9 class ·
22	18, 20, 21	co 7411	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11253	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5147	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17148	. . . . . . . 8 class Base
26	6, 25	cfv 6542	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3059	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11112	. . . . . . 7 class 0
29		cpnf 11249	. . . . . . 7 class +∞
30		cico 13330	. . . . . . 7 class [,)
31	28, 29, 30	co 7411	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3430	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11251	. . . . 5 class ℝ*
34		clt 11252	. . . . 5 class <
35	32, 33, 34	cinf 9438	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5230	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7413	. 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  24448  nmofval  24451