Definition df-nmo 25036

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 25033	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24905	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1568	. . . . 5 class 𝑠
7	3	cv 1568	. . . . 5 class 𝑡
8		cghm 19436	. . . . 5 class GrpHom
9	6, 7, 8	co 7424	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1568	. . . . . . . . . 10 class 𝑥
12	5	cv 1568	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6543	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24904	. . . . . . . . . 10 class norm
15	7, 14	cfv 6543	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6543	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1568	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6543	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6543	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11212	. . . . . . . . 9 class ·
22	18, 20, 21	co 7424	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11351	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5102	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17396	. . . . . . . 8 class Base
26	6, 25	cfv 6543	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3076	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11207	. . . . . . 7 class 0
29		cpnf 11347	. . . . . . 7 class +∞
30		cico 13485	. . . . . . 7 class [,)
31	28, 29, 30	co 7424	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3412	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11349	. . . . 5 class ℝ*
34		clt 11350	. . . . 5 class <
35	32, 33, 34	cinf 9440	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5185	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7426	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1569	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is used by:  nmoffn  25039  nmofval  25042