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 ‘ 𝑠 ) ‘ 𝑥 ) ) } , ℝ* , < ) ) )