Definition df-nmo 24603

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 24600	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24472	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1539	. . . . 5 class 𝑠
7	3	cv 1539	. . . . 5 class 𝑡
8		cghm 19151	. . . . 5 class GrpHom
9	6, 7, 8	co 7390	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1539	. . . . . . . . . 10 class 𝑥
12	5	cv 1539	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6514	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24471	. . . . . . . . . 10 class norm
15	7, 14	cfv 6514	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6514	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1539	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6514	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6514	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11080	. . . . . . . . 9 class ·
22	18, 20, 21	co 7390	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11216	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5110	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17186	. . . . . . . 8 class Base
26	6, 25	cfv 6514	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3045	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11075	. . . . . . 7 class 0
29		cpnf 11212	. . . . . . 7 class +∞
30		cico 13315	. . . . . . 7 class [,)
31	28, 29, 30	co 7390	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3408	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11214	. . . . 5 class ℝ*
34		clt 11215	. . . . 5 class <
35	32, 33, 34	cinf 9399	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5191	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7392	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1540	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24606  nmofval  24609