Definition df-nmo 24650

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 24647	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24519	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1540	. . . . 5 class 𝑠
7	3	cv 1540	. . . . 5 class 𝑡
8		cghm 19139	. . . . 5 class GrpHom
9	6, 7, 8	co 7356	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1540	. . . . . . . . . 10 class 𝑥
12	5	cv 1540	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6490	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24518	. . . . . . . . . 10 class norm
15	7, 14	cfv 6490	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6490	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1540	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6490	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6490	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11029	. . . . . . . . 9 class ·
22	18, 20, 21	co 7356	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11165	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5096	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17134	. . . . . . . 8 class Base
26	6, 25	cfv 6490	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3049	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11024	. . . . . . 7 class 0
29		cpnf 11161	. . . . . . 7 class +∞
30		cico 13261	. . . . . . 7 class [,)
31	28, 29, 30	co 7356	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3397	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11163	. . . . 5 class ℝ*
34		clt 11164	. . . . 5 class <
35	32, 33, 34	cinf 9342	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5177	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7358	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1541	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24653  nmofval  24656