Definition df-nmo 23395

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 23392	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 23264	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . 5 class 𝑠
7	3	cv 1538	. . . . 5 class 𝑡
8		cghm 18407	. . . . 5 class GrpHom
9	6, 7, 8	co 7143	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1538	. . . . . . . . . 10 class 𝑥
12	5	cv 1538	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6328	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 23263	. . . . . . . . . 10 class norm
15	7, 14	cfv 6328	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6328	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1538	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6328	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6328	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 10565	. . . . . . . . 9 class ·
22	18, 20, 21	co 7143	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 10699	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5025	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 16526	. . . . . . . 8 class Base
26	6, 25	cfv 6328	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3068	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 10560	. . . . . . 7 class 0
29		cpnf 10695	. . . . . . 7 class +∞
30		cico 12766	. . . . . . 7 class [,)
31	28, 29, 30	co 7143	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3072	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 10697	. . . . 5 class ℝ*
34		clt 10698	. . . . 5 class <
35	32, 33, 34	cinf 8923	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5105	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7145	. 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  23398  nmofval  23401