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 24729
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 24726 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 24590 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1539 . . . . 5 class 𝑠
73cv 1539 . . . . 5 class 𝑡
8 cghm 19230 . . . . 5 class GrpHom
96, 7, 8co 7431 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1539 . . . . . . . . . 10 class 𝑥
125cv 1539 . . . . . . . . . 10 class 𝑓
1311, 12cfv 6561 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 24589 . . . . . . . . . 10 class norm
157, 14cfv 6561 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 6561 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1539 . . . . . . . . 9 class 𝑟
196, 14cfv 6561 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 6561 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 11160 . . . . . . . . 9 class ·
2218, 20, 21co 7431 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 11296 . . . . . . . 8 class
2416, 22, 23wbr 5143 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 17247 . . . . . . . 8 class Base
266, 25cfv 6561 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 3061 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 11155 . . . . . . 7 class 0
29 cpnf 11292 . . . . . . 7 class +∞
30 cico 13389 . . . . . . 7 class [,)
3128, 29, 30co 7431 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 3436 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 11294 . . . . 5 class *
34 clt 11295 . . . . 5 class <
3532, 33, 34cinf 9481 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 5225 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpo 7433 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1540 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  24732  nmofval  24735
  Copyright terms: Public domain W3C validator