Definition df-nv 21148

Description: Define the class of all normed complex vector spaces. (Contributed by NM, 11-Nov-2006.) (New usage is discouraged.)

Assertion

Ref	Expression
df-nv	|- NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVec OLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }

Distinct variable group:   g, s, n, x, y

Detailed syntax breakdown of Definition df-nv

Step	Hyp	Ref	Expression
1		cnv 21140	. 2 class NrmCVec
2		vg	. . . . . . 7 set g
3	2	cv 1622	. . . . . 6 class g
4		vs	. . . . . . 7 set s
5	4	cv 1622	. . . . . 6 class s
6	3, 5	cop 3643	. . . . 5 class <. g , s >.
7		cvc 21101	. . . . 5 class CVec OLD
8	6, 7	wcel 1684	. . . 4 wff <. g , s >. e. CVec OLD
9	3	crn 4690	. . . . 5 class ran g
10		cr 8736	. . . . 5 class RR
11		vn	. . . . . 6 set n
12	11	cv 1622	. . . . 5 class n
13	9, 10, 12	wf 5251	. . . 4 wff n : ran g --> RR
14		vx	. . . . . . . . . 10 set x
15	14	cv 1622	. . . . . . . . 9 class x
16	15, 12	cfv 5255	. . . . . . . 8 class ( n ` x )
17		cc0 8737	. . . . . . . 8 class 0
18	16, 17	wceq 1623	. . . . . . 7 wff ( n ` x ) = 0
19		cgi 20854	. . . . . . . . 9 class GId
20	3, 19	cfv 5255	. . . . . . . 8 class (GId ` g )
21	15, 20	wceq 1623	. . . . . . 7 wff x = (GId ` g )
22	18, 21	wi 4	. . . . . 6 wff ( ( n ` x ) = 0 -> x = (GId ` g ) )
23		vy	. . . . . . . . . . 11 set y
24	23	cv 1622	. . . . . . . . . 10 class y
25	24, 15, 5	co 5858	. . . . . . . . 9 class ( y s x )
26	25, 12	cfv 5255	. . . . . . . 8 class ( n ` ( y s x ) )
27		cabs 11719	. . . . . . . . . 10 class abs
28	24, 27	cfv 5255	. . . . . . . . 9 class ( abs ` y )
29		cmul 8742	. . . . . . . . 9 class x.
30	28, 16, 29	co 5858	. . . . . . . 8 class ( ( abs ` y ) x. ( n ` x ) )
31	26, 30	wceq 1623	. . . . . . 7 wff ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
32		cc 8735	. . . . . . 7 class CC
33	31, 23, 32	wral 2543	. . . . . 6 wff A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
34	15, 24, 3	co 5858	. . . . . . . . 9 class ( x g y )
35	34, 12	cfv 5255	. . . . . . . 8 class ( n ` ( x g y ) )
36	24, 12	cfv 5255	. . . . . . . . 9 class ( n ` y )
37		caddc 8740	. . . . . . . . 9 class +
38	16, 36, 37	co 5858	. . . . . . . 8 class ( ( n ` x ) + ( n ` y ) )
39		cle 8868	. . . . . . . 8 class <_
40	35, 38, 39	wbr 4023	. . . . . . 7 wff ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
41	40, 23, 9	wral 2543	. . . . . 6 wff A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
42	22, 33, 41	w3a 934	. . . . 5 wff ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) )
43	42, 14, 9	wral 2543	. . . 4 wff A. x e. ran g ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) )
44	8, 13, 43	w3a 934	. . 3 wff ( <. g , s >. e. CVec OLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) )
45	44, 2, 4, 11	coprab 5859	. 2 class { <. <. g , s >. , n >. | ( <. g , s >. e. CVec OLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }
46	1, 45	wceq 1623	1 wff NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVec OLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = (GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) }

This definition is referenced by:  nvss  21149  isnvlem  21166