df-nmo - Metamath Proof Explorer

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

Definition df-nmo 22512

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.) (Revised by AV, 25-Sep-2020.)

**Assertion**
Ref	Expression
df-nmo	NrmGrp NrmGrp inf

Distinct variable group:

**Detailed syntax breakdown of Definition df-nmo**
Step	Hyp	Ref	Expression
1		cnmo 22509	. 2
2		vs	. . 3
3		vt	. . 3
4		cngp 22382	. . 3 NrmGrp
5		vf	. . . 4
6	2	cv 1482	. . . . 5
7	3	cv 1482	. . . . 5
8		cghm 17657	. . . . 5
9	6, 7, 8	co 6650	. . . 4
10		vx	. . . . . . . . . . 11
11	10	cv 1482	. . . . . . . . . 10
12	5	cv 1482	. . . . . . . . . 10
13	11, 12	cfv 5888	. . . . . . . . 9
14		cnm 22381	. . . . . . . . . 10
15	7, 14	cfv 5888	. . . . . . . . 9
16	13, 15	cfv 5888	. . . . . . . 8
17		vr	. . . . . . . . . 10
18	17	cv 1482	. . . . . . . . 9
19	6, 14	cfv 5888	. . . . . . . . . 10
20	11, 19	cfv 5888	. . . . . . . . 9
21		cmul 9941	. . . . . . . . 9
22	18, 20, 21	co 6650	. . . . . . . 8
23		cle 10075	. . . . . . . 8
24	16, 22, 23	wbr 4653	. . . . . . 7
25		cbs 15857	. . . . . . . 8
26	6, 25	cfv 5888	. . . . . . 7
27	24, 10, 26	wral 2912	. . . . . 6
28		cc0 9936	. . . . . . 7
29		cpnf 10071	. . . . . . 7
30		cico 12177	. . . . . . 7
31	28, 29, 30	co 6650	. . . . . 6
32	27, 17, 31	crab 2916	. . . . 5
33		cxr 10073	. . . . 5
34		clt 10074	. . . . 5
35	32, 33, 34	cinf 8347	. . . 4 inf
36	5, 9, 35	cmpt 4729	. . 3 inf
37	2, 3, 4, 4, 36	cmpt2 6652	. 2 NrmGrp NrmGrp inf
38	1, 37	wceq 1483	1 NrmGrp NrmGrp inf

Colors of variables: wff setvar class

This definition is referenced by: nmoffn 22515 nmofval 22518

W3C validator