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 24206
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 24203 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 24067 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1541 . . . . 5 class 𝑠
73cv 1541 . . . . 5 class 𝑡
8 cghm 19082 . . . . 5 class GrpHom
96, 7, 8co 7403 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1541 . . . . . . . . . 10 class 𝑥
125cv 1541 . . . . . . . . . 10 class 𝑓
1311, 12cfv 6539 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 24066 . . . . . . . . . 10 class norm
157, 14cfv 6539 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 6539 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1541 . . . . . . . . 9 class 𝑟
196, 14cfv 6539 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 6539 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 11110 . . . . . . . . 9 class ·
2218, 20, 21co 7403 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 11244 . . . . . . . 8 class
2416, 22, 23wbr 5146 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 17139 . . . . . . . 8 class Base
266, 25cfv 6539 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 3062 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 11105 . . . . . . 7 class 0
29 cpnf 11240 . . . . . . 7 class +∞
30 cico 13321 . . . . . . 7 class [,)
3128, 29, 30co 7403 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 3433 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 11242 . . . . 5 class *
34 clt 11243 . . . . 5 class <
3532, 33, 34cinf 9431 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 5229 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpo 7405 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1542 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  24209  nmofval  24212
  Copyright terms: Public domain W3C validator