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∈sGrpHomt⟼supr∈0+∞|∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡xℝ*<

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmo classnormOp
1 vs setvars
2 cngp classNrmGrp
3 vt setvart
4 vf setvarf
5 1 cv setvars
6 cghm classGrpHom
7 3 cv setvart
8 5 7 6 co classsGrpHomt
9 vr setvarr
10 cc0 class0
11 cico class.
12 cpnf class+∞
13 10 12 11 co class0+∞
14 vx setvarx
15 cbs classBase
16 5 15 cfv classBases
17 cnm classnorm
18 7 17 cfv classnorm⁡t
19 4 cv setvarf
20 14 cv setvarx
21 20 19 cfv classf⁡x
22 21 18 cfv classnorm⁡t⁡f⁡x
23 cle class≤
24 9 cv setvarr
25 cmul class×
26 5 17 cfv classnorm⁡s
27 20 26 cfv classnorm⁡s⁡x
28 24 27 25 co classr⁢norm⁡s⁡x
29 22 28 23 wbr wffnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡x
30 29 14 16 wral wff∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡x
31 30 9 13 crab classr∈0+∞|∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡x
32 cxr classℝ*
33 clt class<
34 31 32 33 cinf classsupr∈0+∞|∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡xℝ*<
35 4 8 34 cmpt classf∈sGrpHomt⟼supr∈0+∞|∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡xℝ*<
36 1 3 2 2 35 cmpo classs∈NrmGrp,t∈NrmGrp⟼f∈sGrpHomt⟼supr∈0+∞|∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡xℝ*<
37 0 36 wceq wffnormOp=s∈NrmGrp,t∈NrmGrp⟼f∈sGrpHomt⟼supr∈0+∞|∀x∈Basesnorm⁡t⁡f⁡x≤r⁢norm⁡s⁡xℝ*<