Definition df-nmo 24673

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 24670	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24542	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1541	. . . . 5 class 𝑠
7	3	cv 1541	. . . . 5 class 𝑡
8		cghm 19187	. . . . 5 class GrpHom
9	6, 7, 8	co 7367	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1541	. . . . . . . . . 10 class 𝑥
12	5	cv 1541	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6498	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24541	. . . . . . . . . 10 class norm
15	7, 14	cfv 6498	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6498	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1541	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6498	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6498	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11043	. . . . . . . . 9 class ·
22	18, 20, 21	co 7367	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11180	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5085	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17179	. . . . . . . 8 class Base
26	6, 25	cfv 6498	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3051	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11038	. . . . . . 7 class 0
29		cpnf 11176	. . . . . . 7 class +∞
30		cico 13300	. . . . . . 7 class [,)
31	28, 29, 30	co 7367	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3389	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11178	. . . . 5 class ℝ*
34		clt 11179	. . . . 5 class <
35	32, 33, 34	cinf 9354	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5166	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7369	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1542	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24676  nmofval  24679