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 23309
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 23306 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 23179 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1529 . . . . 5 class 𝑠
73cv 1529 . . . . 5 class 𝑡
8 cghm 18347 . . . . 5 class GrpHom
96, 7, 8co 7148 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1529 . . . . . . . . . 10 class 𝑥
125cv 1529 . . . . . . . . . 10 class 𝑓
1311, 12cfv 6348 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 23178 . . . . . . . . . 10 class norm
157, 14cfv 6348 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 6348 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1529 . . . . . . . . 9 class 𝑟
196, 14cfv 6348 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 6348 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 10534 . . . . . . . . 9 class ·
2218, 20, 21co 7148 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 10668 . . . . . . . 8 class
2416, 22, 23wbr 5057 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 16475 . . . . . . . 8 class Base
266, 25cfv 6348 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 3136 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 10529 . . . . . . 7 class 0
29 cpnf 10664 . . . . . . 7 class +∞
30 cico 12732 . . . . . . 7 class [,)
3128, 29, 30co 7148 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 3140 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 10666 . . . . 5 class *
34 clt 10667 . . . . 5 class <
3532, 33, 34cinf 8897 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 5137 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpo 7150 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1530 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  23312  nmofval  23315
  Copyright terms: Public domain W3C validator