Definition df-nmo 23778

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 23775	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 23639	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . 5 class 𝑠
7	3	cv 1538	. . . . 5 class 𝑡
8		cghm 18746	. . . . 5 class GrpHom
9	6, 7, 8	co 7255	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1538	. . . . . . . . . 10 class 𝑥
12	5	cv 1538	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6418	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 23638	. . . . . . . . . 10 class norm
15	7, 14	cfv 6418	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6418	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1538	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6418	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6418	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 10807	. . . . . . . . 9 class ·
22	18, 20, 21	co 7255	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 10941	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5070	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 16840	. . . . . . . 8 class Base
26	6, 25	cfv 6418	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3063	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 10802	. . . . . . 7 class 0
29		cpnf 10937	. . . . . . 7 class +∞
30		cico 13010	. . . . . . 7 class [,)
31	28, 29, 30	co 7255	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3067	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 10939	. . . . 5 class ℝ*
34		clt 10940	. . . . 5 class <
35	32, 33, 34	cinf 9130	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5153	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7257	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1539	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  23781  nmofval  23784