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 22837
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 22834 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 22707 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1652 . . . . 5 class 𝑠
73cv 1652 . . . . 5 class 𝑡
8 cghm 17967 . . . . 5 class GrpHom
96, 7, 8co 6877 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1652 . . . . . . . . . 10 class 𝑥
125cv 1652 . . . . . . . . . 10 class 𝑓
1311, 12cfv 6100 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 22706 . . . . . . . . . 10 class norm
157, 14cfv 6100 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 6100 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1652 . . . . . . . . 9 class 𝑟
196, 14cfv 6100 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 6100 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 10228 . . . . . . . . 9 class ·
2218, 20, 21co 6877 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 10363 . . . . . . . 8 class
2416, 22, 23wbr 4842 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 16181 . . . . . . . 8 class Base
266, 25cfv 6100 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 3088 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 10223 . . . . . . 7 class 0
29 cpnf 10359 . . . . . . 7 class +∞
30 cico 12423 . . . . . . 7 class [,)
3128, 29, 30co 6877 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 3092 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 10361 . . . . 5 class *
34 clt 10362 . . . . 5 class <
3532, 33, 34cinf 8588 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 4921 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpt2 6879 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1653 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  22840  nmofval  22843
  Copyright terms: Public domain W3C validator