Definition df-nv 27447

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. CVecOLD /\ 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 27439	. 2 class NrmCVec
2		vg	. . . . . . 7 setvar g
3	2	cv 1482	. . . . . 6 class g
4		vs	. . . . . . 7 setvar s
5	4	cv 1482	. . . . . 6 class s
6	3, 5	cop 4183	. . . . 5 class <. g , s >.
7		cvc 27413	. . . . 5 class CVecOLD
8	6, 7	wcel 1990	. . . 4 wff <. g , s >. e. CVecOLD
9	3	crn 5115	. . . . 5 class ran g
10		cr 9935	. . . . 5 class RR
11		vn	. . . . . 6 setvar n
12	11	cv 1482	. . . . 5 class n
13	9, 10, 12	wf 5884	. . . 4 wff n : ran g --> RR
14		vx	. . . . . . . . . 10 setvar x
15	14	cv 1482	. . . . . . . . 9 class x
16	15, 12	cfv 5888	. . . . . . . 8 class ( n ` x )
17		cc0 9936	. . . . . . . 8 class 0
18	16, 17	wceq 1483	. . . . . . 7 wff ( n ` x ) = 0
19		cgi 27344	. . . . . . . . 9 class GId
20	3, 19	cfv 5888	. . . . . . . 8 class (GId ` g )
21	15, 20	wceq 1483	. . . . . . 7 wff x = (GId ` g )
22	18, 21	wi 4	. . . . . 6 wff ( ( n ` x ) = 0 -> x = (GId ` g ) )
23		vy	. . . . . . . . . . 11 setvar y
24	23	cv 1482	. . . . . . . . . 10 class y
25	24, 15, 5	co 6650	. . . . . . . . 9 class ( y s x )
26	25, 12	cfv 5888	. . . . . . . 8 class ( n ` ( y s x ) )
27		cabs 13974	. . . . . . . . . 10 class abs
28	24, 27	cfv 5888	. . . . . . . . 9 class ( abs ` y )
29		cmul 9941	. . . . . . . . 9 class x.
30	28, 16, 29	co 6650	. . . . . . . 8 class ( ( abs ` y ) x. ( n ` x ) )
31	26, 30	wceq 1483	. . . . . . 7 wff ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
32		cc 9934	. . . . . . 7 class CC
33	31, 23, 32	wral 2912	. . . . . 6 wff A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
34	15, 24, 3	co 6650	. . . . . . . . 9 class ( x g y )
35	34, 12	cfv 5888	. . . . . . . 8 class ( n ` ( x g y ) )
36	24, 12	cfv 5888	. . . . . . . . 9 class ( n ` y )
37		caddc 9939	. . . . . . . . 9 class +
38	16, 36, 37	co 6650	. . . . . . . 8 class ( ( n ` x ) + ( n ` y ) )
39		cle 10075	. . . . . . . 8 class <_
40	35, 38, 39	wbr 4653	. . . . . . 7 wff ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
41	40, 23, 9	wral 2912	. . . . . 6 wff A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
42	22, 33, 41	w3a 1037	. . . . 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 2912	. . . 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 1037	. . 3 wff ( <. g , s >. e. CVecOLD /\ 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 6651	. 2 class { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ 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 1483	1 wff NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ 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  27448  isnvlem  27465