Definition df-nmo 24691

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 24688	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24560	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1546	. . . . 5 class 𝑠
7	3	cv 1546	. . . . 5 class 𝑡
8		cghm 19178	. . . . 5 class GrpHom
9	6, 7, 8	co 7356	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1546	. . . . . . . . . 10 class 𝑥
12	5	cv 1546	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6485	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24559	. . . . . . . . . 10 class norm
15	7, 14	cfv 6485	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6485	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1546	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6485	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6485	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11034	. . . . . . . . 9 class ·
22	18, 20, 21	co 7356	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11171	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5072	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17170	. . . . . . . 8 class Base
26	6, 25	cfv 6485	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3053	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11029	. . . . . . 7 class 0
29		cpnf 11167	. . . . . . 7 class +∞
30		cico 13291	. . . . . . 7 class [,)
31	28, 29, 30	co 7356	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3391	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11169	. . . . 5 class ℝ*
34		clt 11170	. . . . 5 class <
35	32, 33, 34	cinf 9344	. . . 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 7358	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1547	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24694  nmofval  24697