Definition df-nmo 23319

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 23316	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 23189	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1536	. . . . 5 class 𝑠
7	3	cv 1536	. . . . 5 class 𝑡
8		cghm 18357	. . . . 5 class GrpHom
9	6, 7, 8	co 7158	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1536	. . . . . . . . . 10 class 𝑥
12	5	cv 1536	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6357	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 23188	. . . . . . . . . 10 class norm
15	7, 14	cfv 6357	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6357	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1536	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6357	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6357	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 10544	. . . . . . . . 9 class ·
22	18, 20, 21	co 7158	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 10678	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5068	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 16485	. . . . . . . 8 class Base
26	6, 25	cfv 6357	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3140	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 10539	. . . . . . 7 class 0
29		cpnf 10674	. . . . . . 7 class +∞
30		cico 12743	. . . . . . 7 class [,)
31	28, 29, 30	co 7158	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3144	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 10676	. . . . 5 class ℝ*
34		clt 10677	. . . . 5 class <
35	32, 33, 34	cinf 8907	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5148	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7160	. 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  23322  nmofval  23325