Metamath Proof Explorer


Definition df-nmo

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 <. s , t >. . 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)

Ref Expression
Assertion df-nmo normOp = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmo normOp
1 vs 𝑠
2 cngp NrmGrp
3 vt 𝑡
4 vf 𝑓
5 1 cv 𝑠
6 cghm GrpHom
7 3 cv 𝑡
8 5 7 6 co ( 𝑠 GrpHom 𝑡 )
9 vr 𝑟
10 cc0 0
11 cico [,)
12 cpnf +∞
13 10 12 11 co ( 0 [,) +∞ )
14 vx 𝑥
15 cbs Base
16 5 15 cfv ( Base ‘ 𝑠 )
17 cnm norm
18 7 17 cfv ( norm ‘ 𝑡 )
19 4 cv 𝑓
20 14 cv 𝑥
21 20 19 cfv ( 𝑓𝑥 )
22 21 18 cfv ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) )
23 cle
24 9 cv 𝑟
25 cmul ·
26 5 17 cfv ( norm ‘ 𝑠 )
27 20 26 cfv ( ( norm ‘ 𝑠 ) ‘ 𝑥 )
28 24 27 25 co ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) )
29 22 28 23 wbr ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) )
30 29 14 16 wral 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) )
31 30 9 13 crab { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) }
32 cxr *
33 clt <
34 31 32 33 cinf inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < )
35 4 8 34 cmpt ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) )
36 1 3 2 2 35 cmpo ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )
37 0 36 wceq normOp = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( 𝑓 ∈ ( 𝑠 GrpHom 𝑡 ) ↦ inf ( { 𝑟 ∈ ( 0 [,) +∞ ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ( ( norm ‘ 𝑡 ) ‘ ( 𝑓𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )