Definition df-nv 22032

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 22024	. 2 class NrmCVec
2		vg	. . . . . . 7 set g
3	2	cv 1648	. . . . . 6 class g
4		vs	. . . . . . 7 set s
5	4	cv 1648	. . . . . 6 class s
6	3, 5	cop 3785	. . . . 5 class <. g , s >.
7		cvc 21985	. . . . 5 class CVec OLD
8	6, 7	wcel 1721	. . . 4 wff <. g , s >. e. CVec OLD
9	3	crn 4846	. . . . 5 class ran g
10		cr 8953	. . . . 5 class RR
11		vn	. . . . . 6 set n
12	11	cv 1648	. . . . 5 class n
13	9, 10, 12	wf 5417	. . . 4 wff n : ran g --> RR
14		vx	. . . . . . . . . 10 set x
15	14	cv 1648	. . . . . . . . 9 class x
16	15, 12	cfv 5421	. . . . . . . 8 class ( n ` x )
17		cc0 8954	. . . . . . . 8 class 0
18	16, 17	wceq 1649	. . . . . . 7 wff ( n ` x ) = 0
19		cgi 21736	. . . . . . . . 9 class GId
20	3, 19	cfv 5421	. . . . . . . 8 class (GId ` g )
21	15, 20	wceq 1649	. . . . . . 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 1648	. . . . . . . . . 10 class y
25	24, 15, 5	co 6048	. . . . . . . . 9 class ( y s x )
26	25, 12	cfv 5421	. . . . . . . 8 class ( n ` ( y s x ) )
27		cabs 12002	. . . . . . . . . 10 class abs
28	24, 27	cfv 5421	. . . . . . . . 9 class ( abs ` y )
29		cmul 8959	. . . . . . . . 9 class x.
30	28, 16, 29	co 6048	. . . . . . . 8 class ( ( abs ` y ) x. ( n ` x ) )
31	26, 30	wceq 1649	. . . . . . 7 wff ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
32		cc 8952	. . . . . . 7 class CC
33	31, 23, 32	wral 2674	. . . . . 6 wff A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) )
34	15, 24, 3	co 6048	. . . . . . . . 9 class ( x g y )
35	34, 12	cfv 5421	. . . . . . . 8 class ( n ` ( x g y ) )
36	24, 12	cfv 5421	. . . . . . . . 9 class ( n ` y )
37		caddc 8957	. . . . . . . . 9 class +
38	16, 36, 37	co 6048	. . . . . . . 8 class ( ( n ` x ) + ( n ` y ) )
39		cle 9085	. . . . . . . 8 class <_
40	35, 38, 39	wbr 4180	. . . . . . 7 wff ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
41	40, 23, 9	wral 2674	. . . . . 6 wff A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) )
42	22, 33, 41	w3a 936	. . . . 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 2674	. . . 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 936	. . 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 6049	. 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 1649	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  22033  isnvlem  22050