Definition df-nmo 24865

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 24862	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24734	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1569	. . . . 5 class 𝑠
7	3	cv 1569	. . . . 5 class 𝑡
8		cghm 19278	. . . . 5 class GrpHom
9	6, 7, 8	co 7410	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1569	. . . . . . . . . 10 class 𝑥
12	5	cv 1569	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6536	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24733	. . . . . . . . . 10 class norm
15	7, 14	cfv 6536	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6536	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1569	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6536	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6536	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11100	. . . . . . . . 9 class ·
22	18, 20, 21	co 7410	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11239	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5109	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17264	. . . . . . . 8 class Base
26	6, 25	cfv 6536	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3079	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11095	. . . . . . 7 class 0
29		cpnf 11235	. . . . . . 7 class +∞
30		cico 13369	. . . . . . 7 class [,)
31	28, 29, 30	co 7410	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3416	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11237	. . . . 5 class ℝ*
34		clt 11238	. . . . 5 class <
35	32, 33, 34	cinf 9397	. . . 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 7412	. 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 referenced by:  nmoffn  24868  nmofval  24871