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 22506
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 22503 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cngp 22376 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1481 . . . . 5 class 𝑠
73cv 1481 . . . . 5 class 𝑡
8 cghm 17651 . . . . 5 class GrpHom
96, 7, 8co 6647 . . . 4 class (𝑠 GrpHom 𝑡)
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1481 . . . . . . . . . 10 class 𝑥
125cv 1481 . . . . . . . . . 10 class 𝑓
1311, 12cfv 5886 . . . . . . . . 9 class (𝑓𝑥)
14 cnm 22375 . . . . . . . . . 10 class norm
157, 14cfv 5886 . . . . . . . . 9 class (norm‘𝑡)
1613, 15cfv 5886 . . . . . . . 8 class ((norm‘𝑡)‘(𝑓𝑥))
17 vr . . . . . . . . . 10 setvar 𝑟
1817cv 1481 . . . . . . . . 9 class 𝑟
196, 14cfv 5886 . . . . . . . . . 10 class (norm‘𝑠)
2011, 19cfv 5886 . . . . . . . . 9 class ((norm‘𝑠)‘𝑥)
21 cmul 9938 . . . . . . . . 9 class ·
2218, 20, 21co 6647 . . . . . . . 8 class (𝑟 · ((norm‘𝑠)‘𝑥))
23 cle 10072 . . . . . . . 8 class
2416, 22, 23wbr 4651 . . . . . . 7 wff ((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
25 cbs 15851 . . . . . . . 8 class Base
266, 25cfv 5886 . . . . . . 7 class (Base‘𝑠)
2724, 10, 26wral 2911 . . . . . 6 wff 𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))
28 cc0 9933 . . . . . . 7 class 0
29 cpnf 10068 . . . . . . 7 class +∞
30 cico 12174 . . . . . . 7 class [,)
3128, 29, 30co 6647 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 2915 . . . . 5 class {𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}
33 cxr 10070 . . . . 5 class *
34 clt 10071 . . . . 5 class <
3532, 33, 34cinf 8344 . . . 4 class inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )
365, 9, 35cmpt 4727 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < ))
372, 3, 4, 4, 36cmpt2 6649 . 2 class (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
381, 37wceq 1482 1 wff normOp = (𝑠 ∈ NrmGrp, 𝑡 ∈ NrmGrp ↦ (𝑓 ∈ (𝑠 GrpHom 𝑡) ↦ inf({𝑟 ∈ (0[,)+∞) ∣ ∀𝑥 ∈ (Base‘𝑠)((norm‘𝑡)‘(𝑓𝑥)) ≤ (𝑟 · ((norm‘𝑠)‘𝑥))}, ℝ*, < )))
Colors of variables: wff setvar class
This definition is referenced by:  nmoffn  22509  nmofval  22512
  Copyright terms: Public domain W3C validator