Definition df-nmo 24916

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 24913	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24785	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1569	. . . . 5 class 𝑠
7	3	cv 1569	. . . . 5 class 𝑡
8		cghm 19327	. . . . 5 class GrpHom
9	6, 7, 8	co 7419	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1569	. . . . . . . . . 10 class 𝑥
12	5	cv 1569	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6540	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24784	. . . . . . . . . 10 class norm
15	7, 14	cfv 6540	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6540	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1569	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6540	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6540	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11120	. . . . . . . . 9 class ·
22	18, 20, 21	co 7419	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11259	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5111	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17291	. . . . . . . 8 class Base
26	6, 25	cfv 6540	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3081	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11115	. . . . . . 7 class 0
29		cpnf 11255	. . . . . . 7 class +∞
30		cico 13390	. . . . . . 7 class [,)
31	28, 29, 30	co 7419	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3418	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11257	. . . . 5 class ℝ*
34		clt 11258	. . . . 5 class <
35	32, 33, 34	cinf 9408	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5194	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7421	. 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  24919  nmofval  24922