Definition df-nmo 24833

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 24830	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24702	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1566	. . . . 5 class 𝑠
7	3	cv 1566	. . . . 5 class 𝑡
8		cghm 19282	. . . . 5 class GrpHom
9	6, 7, 8	co 7411	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1566	. . . . . . . . . 10 class 𝑥
12	5	cv 1566	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6537	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24701	. . . . . . . . . 10 class norm
15	7, 14	cfv 6537	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6537	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1566	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6537	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6537	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11104	. . . . . . . . 9 class ·
22	18, 20, 21	co 7411	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11243	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5113	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17268	. . . . . . . 8 class Base
26	6, 25	cfv 6537	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3085	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11099	. . . . . . 7 class 0
29		cpnf 11239	. . . . . . 7 class +∞
30		cico 13373	. . . . . . 7 class [,)
31	28, 29, 30	co 7411	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3423	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11241	. . . . 5 class ℝ*
34		clt 11242	. . . . 5 class <
35	32, 33, 34	cinf 9400	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5196	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7413	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1567	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is referenced by:  nmoffn  24836  nmofval  24839