Definition df-nmo 24664

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 24661	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24533	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1541	. . . . 5 class 𝑠
7	3	cv 1541	. . . . 5 class 𝑡
8		cghm 19153	. . . . 5 class GrpHom
9	6, 7, 8	co 7368	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1541	. . . . . . . . . 10 class 𝑥
12	5	cv 1541	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6500	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24532	. . . . . . . . . 10 class norm
15	7, 14	cfv 6500	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6500	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1541	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6500	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6500	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11043	. . . . . . . . 9 class ·
22	18, 20, 21	co 7368	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11179	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5100	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17148	. . . . . . . 8 class Base
26	6, 25	cfv 6500	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3052	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11038	. . . . . . 7 class 0
29		cpnf 11175	. . . . . . 7 class +∞
30		cico 13275	. . . . . . 7 class [,)
31	28, 29, 30	co 7368	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3401	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11177	. . . . 5 class ℝ*
34		clt 11178	. . . . 5 class <
35	32, 33, 34	cinf 9356	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5181	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7370	. 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  24667  nmofval  24670