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 = s ∈ NrmGrp , t ∈ NrmGrp ⟼ f ∈ s GrpHom t ⟼ inf r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmo class normOp
1 vs setvar s
2 cngp class NrmGrp
3 vt setvar t
4 vf setvar f
5 1 cv setvar s
6 cghm class GrpHom
7 3 cv setvar t
8 5 7 6 co class s GrpHom t
9 vr setvar r
10 cc0 class 0
11 cico class .
12 cpnf class +∞
13 10 12 11 co class 0 +∞
14 vx setvar x
15 cbs class Base
16 5 15 cfv class Base s
17 cnm class norm
18 7 17 cfv class norm ⁡ t
19 4 cv setvar f
20 14 cv setvar x
21 20 19 cfv class f ⁡ x
22 21 18 cfv class norm ⁡ t ⁡ f ⁡ x
23 cle class ≤
24 9 cv setvar r
25 cmul class ×
26 5 17 cfv class norm ⁡ s
27 20 26 cfv class norm ⁡ s ⁡ x
28 24 27 25 co class r ⁢ norm ⁡ s ⁡ x
29 22 28 23 wbr wff norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x
30 29 14 16 wral wff ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x
31 30 9 13 crab class r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x
32 cxr class ℝ *
33 clt class <
34 31 32 33 cinf class inf r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <
35 4 8 34 cmpt class f ∈ s GrpHom t ⟼ inf r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <
36 1 3 2 2 35 cmpo class s ∈ NrmGrp , t ∈ NrmGrp ⟼ f ∈ s GrpHom t ⟼ inf r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <
37 0 36 wceq wff normOp = s ∈ NrmGrp , t ∈ NrmGrp ⟼ f ∈ s GrpHom t ⟼ inf r ∈ 0 +∞ | ∀ x ∈ Base s norm ⁡ t ⁡ f ⁡ x ≤ r ⁢ norm ⁡ s ⁡ x ℝ * <