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 22732
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 22729 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 22602 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1630 . . . . 5 class 𝑠
73cv 1630 . . . . 5 class 𝑡
8 cghm 17865 . . . . 5 class GrpHom
96, 7, 8co 6793 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1630 . . . . . . . . . 10 class 𝑥
125cv 1630 . . . . . . . . . 10 class 𝑓
1311, 12cfv 6031 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 22601 . . . . . . . . . 10 class norm
157, 14cfv 6031 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 6031 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1630 . . . . . . . . 9 class 𝑟
196, 14cfv 6031 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 6031 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 10143 . . . . . . . . 9 class ·
2218, 20, 21co 6793 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 10277 . . . . . . . 8 class
2416, 22, 23wbr 4786 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 16064 . . . . . . . 8 class Base
266, 25cfv 6031 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 3061 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 10138 . . . . . . 7 class 0
29 cpnf 10273 . . . . . . 7 class +∞
30 cico 12382 . . . . . . 7 class [,)
3128, 29, 30co 6793 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 3065 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 10275 . . . . 5 class *
34 clt 10276 . . . . 5 class <
3532, 33, 34cinf 8503 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 4863 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpt2 6795 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1631 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  22735  nmofval  22738
  Copyright terms: Public domain W3C validator