Definition df-nmo 24594

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 24591	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24463	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1539	. . . . 5 class 𝑠
7	3	cv 1539	. . . . 5 class 𝑡
8		cghm 19091	. . . . 5 class GrpHom
9	6, 7, 8	co 7349	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1539	. . . . . . . . . 10 class 𝑥
12	5	cv 1539	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6482	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24462	. . . . . . . . . 10 class norm
15	7, 14	cfv 6482	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6482	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1539	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6482	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6482	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11014	. . . . . . . . 9 class ·
22	18, 20, 21	co 7349	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11150	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5092	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17120	. . . . . . . 8 class Base
26	6, 25	cfv 6482	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3044	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11009	. . . . . . 7 class 0
29		cpnf 11146	. . . . . . 7 class +∞
30		cico 13250	. . . . . . 7 class [,)
31	28, 29, 30	co 7349	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3394	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11148	. . . . 5 class ℝ*
34		clt 11149	. . . . 5 class <
35	32, 33, 34	cinf 9331	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5173	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7351	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1540	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24597  nmofval  24600