MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nmo Structured version   Visualization version   GIF version

Definition df-nmo 22322
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
StepHypRef Expression
1 cnmo 22319 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 22192 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1474 . . . . 5 class 𝑠
73cv 1474 . . . . 5 class 𝑡
8 cghm 17480 . . . . 5 class GrpHom
96, 7, 8co 6549 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1474 . . . . . . . . . 10 class 𝑥
125cv 1474 . . . . . . . . . 10 class 𝑓
1311, 12cfv 5804 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 22191 . . . . . . . . . 10 class norm
157, 14cfv 5804 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 5804 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1474 . . . . . . . . 9 class 𝑟
196, 14cfv 5804 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 5804 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 9820 . . . . . . . . 9 class ·
2218, 20, 21co 6549 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 9954 . . . . . . . 8 class
2416, 22, 23wbr 4583 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 15695 . . . . . . . 8 class Base
266, 25cfv 5804 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 2896 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 9815 . . . . . . 7 class 0
29 cpnf 9950 . . . . . . 7 class +∞
30 cico 12048 . . . . . . 7 class [,)
3128, 29, 30co 6549 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 2900 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 9952 . . . . 5 class *
34 clt 9953 . . . . 5 class <
3532, 33, 34cinf 8230 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 4643 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpt2 6551 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1475 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  22325  nmofval  22328
  Copyright terms: Public domain W3C validator