Definition df-nmo 24934

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 24931	. 2 class normOp
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cngp 24803	. . 3 class NrmGrp
5		vf	. . . 4 setvar 𝑓
6	2	cv 1569	. . . . 5 class 𝑠
7	3	cv 1569	. . . . 5 class 𝑡
8		cghm 19340	. . . . 5 class GrpHom
9	6, 7, 8	co 7413	. . . 4 class (𝑠 GrpHom 𝑡)
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1569	. . . . . . . . . 10 class 𝑥
12	5	cv 1569	. . . . . . . . . 10 class 𝑓
13	11, 12	cfv 6533	. . . . . . . . 9 class (𝑓‘𝑥)
14		cnm 24802	. . . . . . . . . 10 class norm
15	7, 14	cfv 6533	. . . . . . . . 9 class (norm‘𝑡)
16	13, 15	cfv 6533	. . . . . . . 8 class ((norm‘𝑡)‘(𝑓‘𝑥))
17		vr	. . . . . . . . . 10 setvar 𝑟
18	17	cv 1569	. . . . . . . . 9 class 𝑟
19	6, 14	cfv 6533	. . . . . . . . . 10 class (norm‘𝑠)
20	11, 19	cfv 6533	. . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21		cmul 11129	. . . . . . . . 9 class ·
22	18, 20, 21	co 7413	. . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23		cle 11268	. . . . . . . 8 class ≤
24	16, 22, 23	wbr 5103	. . . . . . 7 wff ((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25		cbs 17301	. . . . . . . 8 class Base
26	6, 25	cfv 6533	. . . . . . 7 class (Base‘𝑠)
27	24, 10, 26	wral 3076	. . . . . 6 wff ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28		cc0 11124	. . . . . . 7 class 0
29		cpnf 11264	. . . . . . 7 class +∞
30		cico 13400	. . . . . . 7 class [,)
31	28, 29, 30	co 7413	. . . . . 6 class (0[,)+∞)
32	27, 17, 31	crab 3412	. . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33		cxr 11266	. . . . 5 class ℝ*
34		clt 11267	. . . . 5 class <
35	32, 33, 34	cinf 9411	. . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
36	5, 9, 35	cmpt 5186	. . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
37	2, 3, 4, 4, 36	cmpo 7415	. 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
38	1, 37	wceq 1570	1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓‘𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))

This definition is used by:  nmoffn  24937  nmofval  24940