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 24095
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 24092 . 2 class normOp
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑑
4 cngp 23956 . . 3 class NrmGrp
5 vf . . . 4 setvar 𝑓
62cv 1541 . . . . 5 class 𝑠
73cv 1541 . . . . 5 class 𝑑
8 cghm 19013 . . . . 5 class GrpHom
96, 7, 8co 7361 . . . 4 class (𝑠 GrpHom 𝑑)
10 vx . . . . . . . . . . 11 setvar π‘₯
1110cv 1541 . . . . . . . . . 10 class π‘₯
125cv 1541 . . . . . . . . . 10 class 𝑓
1311, 12cfv 6500 . . . . . . . . 9 class (π‘“β€˜π‘₯)
14 cnm 23955 . . . . . . . . . 10 class norm
157, 14cfv 6500 . . . . . . . . 9 class (normβ€˜π‘‘)
1613, 15cfv 6500 . . . . . . . 8 class ((normβ€˜π‘‘)β€˜(π‘“β€˜π‘₯))
17 vr . . . . . . . . . 10 setvar π‘Ÿ
1817cv 1541 . . . . . . . . 9 class π‘Ÿ
196, 14cfv 6500 . . . . . . . . . 10 class (normβ€˜π‘ )
2011, 19cfv 6500 . . . . . . . . 9 class ((normβ€˜π‘ )β€˜π‘₯)
21 cmul 11064 . . . . . . . . 9 class Β·
2218, 20, 21co 7361 . . . . . . . 8 class (π‘Ÿ Β· ((normβ€˜π‘ )β€˜π‘₯))
23 cle 11198 . . . . . . . 8 class ≀
2416, 22, 23wbr 5109 . . . . . . 7 wff ((normβ€˜π‘‘)β€˜(π‘“β€˜π‘₯)) ≀ (π‘Ÿ Β· ((normβ€˜π‘ )β€˜π‘₯))
25 cbs 17091 . . . . . . . 8 class Base
266, 25cfv 6500 . . . . . . 7 class (Baseβ€˜π‘ )
2724, 10, 26wral 3061 . . . . . 6 wff βˆ€π‘₯ ∈ (Baseβ€˜π‘ )((normβ€˜π‘‘)β€˜(π‘“β€˜π‘₯)) ≀ (π‘Ÿ Β· ((normβ€˜π‘ )β€˜π‘₯))
28 cc0 11059 . . . . . . 7 class 0
29 cpnf 11194 . . . . . . 7 class +∞
30 cico 13275 . . . . . . 7 class [,)
3128, 29, 30co 7361 . . . . . 6 class (0[,)+∞)
3227, 17, 31crab 3406 . . . . 5 class {π‘Ÿ ∈ (0[,)+∞) ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘ )((normβ€˜π‘‘)β€˜(π‘“β€˜π‘₯)) ≀ (π‘Ÿ Β· ((normβ€˜π‘ )β€˜π‘₯))}
33 cxr 11196 . . . . 5 class ℝ*
34 clt 11197 . . . . 5 class <
3532, 33, 34cinf 9385 . . . 4 class inf({π‘Ÿ ∈ (0[,)+∞) ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘ )((normβ€˜π‘‘)β€˜(π‘“β€˜π‘₯)) ≀ (π‘Ÿ Β· ((normβ€˜π‘ )β€˜π‘₯))}, ℝ*, < )
365, 9, 35cmpt 5192 . . 3 class (𝑓 ∈ (𝑠 GrpHom 𝑑) ↦ inf({π‘Ÿ ∈ (0[,)+∞) ∣ βˆ€π‘₯ ∈ (Baseβ€˜π‘ )((normβ€˜π‘‘)β€˜(π‘“β€˜π‘₯)) ≀ (π‘Ÿ Β· ((normβ€˜π‘ )β€˜π‘₯))}, ℝ*, < ))
372, 3, 4, 4, 36cmpo 7363 . 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  24098  nmofval  24101
  Copyright terms: Public domain W3C validator