Definition df-nmo 25082

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 25079	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24951	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1569	. . . . 5 class 𝑠
7	3	cv 1569	. . . . 5 class 𝑡
8		cghm 19477	. . . . 5 class GrpHom
9	6, 7, 8	co 7451	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1569	. . . . . . . . . 10 class 𝑥
12	5	cv 1569	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6566	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24950	. . . . . . . . . 10 class norm
15	7, 14	cfv 6566	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6566	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1569	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6566	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6566	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11244	. . . . . . . . 9 class ·
22	18, 20, 21	co 7451	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11383	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5108	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17431	. . . . . . . 8 class Base
26	6, 25	cfv 6566	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3080	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11239	. . . . . . 7 class 0
29		cpnf 11379	. . . . . . 7 class +∞
30		cico 13518	. . . . . . 7 class [,)
31	28, 29, 30	co 7451	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3416	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11381	. . . . 5 class ℝ*
34		clt 11382	. . . . 5 class <
35	32, 33, 34	cinf 9470	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5192	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7453	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1570	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is used by:  nmoffn  25085  nmofval  25088