Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nmo Unicode version

Definition df-nmo 18217
 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.)
Assertion
Ref Expression
df-nmo NrmGrp NrmGrp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-nmo
StepHypRef Expression
1 cnmo 18214 . 2
2 vs . . 3
3 vt . . 3
4 cngp 18100 . . 3 NrmGrp
5 vf . . . 4
62cv 1622 . . . . 5
73cv 1622 . . . . 5
8 cghm 14680 . . . . 5
96, 7, 8co 5858 . . . 4
10 vx . . . . . . . . . . 11
1110cv 1622 . . . . . . . . . 10
125cv 1622 . . . . . . . . . 10
1311, 12cfv 5255 . . . . . . . . 9
14 cnm 18099 . . . . . . . . . 10
157, 14cfv 5255 . . . . . . . . 9
1613, 15cfv 5255 . . . . . . . 8
17 vr . . . . . . . . . 10
1817cv 1622 . . . . . . . . 9
196, 14cfv 5255 . . . . . . . . . 10
2011, 19cfv 5255 . . . . . . . . 9
21 cmul 8742 . . . . . . . . 9
2218, 20, 21co 5858 . . . . . . . 8
23 cle 8868 . . . . . . . 8
2416, 22, 23wbr 4023 . . . . . . 7
25 cbs 13148 . . . . . . . 8
266, 25cfv 5255 . . . . . . 7
2724, 10, 26wral 2543 . . . . . 6
28 cc0 8737 . . . . . . 7
29 cpnf 8864 . . . . . . 7
30 cico 10658 . . . . . . 7
3128, 29, 30co 5858 . . . . . 6
3227, 17, 31crab 2547 . . . . 5
33 cxr 8866 . . . . 5
34 clt 8867 . . . . . 6
3534ccnv 4688 . . . . 5
3632, 33, 35csup 7193 . . . 4
375, 9, 36cmpt 4077 . . 3
382, 3, 4, 4, 37cmpt2 5860 . 2 NrmGrp NrmGrp
391, 38wceq 1623 1 NrmGrp NrmGrp
 Colors of variables: wff set class This definition is referenced by:  nmoffn  18220  nmofval  18223
 Copyright terms: Public domain W3C validator