Definition df-nv 8149

Description: Define the class of all normed complex vector spaces.

Assertion

Ref	Expression
df-nv	|- NrmCVec = {<.<.g, s>., n>. | (<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((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 8141	. 2 class NrmCVec
2		vg	. . . . . . 7 set g
3	2	cv 952	. . . . . 6 class g
4		vs	. . . . . . 7 set s
5	4	cv 952	. . . . . 6 class s
6	3, 5	cop 2401	. . . . 5 class <.g, s>.
7		cvc 8101	. . . . 5 class CVec
8	6, 7	wcel 955	. . . 4 wff <.g, s>. e. CVec
9	3	crn 3161	. . . . 5 class ran g
10		cr 5205	. . . . 5 class RR
11		vn	. . . . . 6 set n
12	11	cv 952	. . . . 5 class n
13	9, 10, 12	wf 3168	. . . 4 wff n:ran g-->RR
14		vx	. . . . . . . . . 10 set x
15	14	cv 952	. . . . . . . . 9 class x
16	15, 12	cfv 3172	. . . . . . . 8 class (n` x)
17		cc0 5206	. . . . . . . 8 class 0
18	16, 17	wceq 953	. . . . . . 7 wff (n` x) = 0
19		cgi 7968	. . . . . . . . 9 class Id
20	3, 19	cfv 3172	. . . . . . . 8 class (Id` g)
21	15, 20	wceq 953	. . . . . . 7 wff x = (Id` g)
22	18, 21	wi 3	. . . . . 6 wff ((n` x) = 0 -> x = (Id` g))
23		vy	. . . . . . . . . . 11 set y
24	23	cv 952	. . . . . . . . . 10 class y
25	24, 15, 5	co 3948	. . . . . . . . 9 class (ysx)
26	25, 12	cfv 3172	. . . . . . . 8 class (n` (ysx))
27		cabs 6681	. . . . . . . . . 10 class abs
28	24, 27	cfv 3172	. . . . . . . . 9 class (abs` y)
29		cmul 5211	. . . . . . . . 9 class x.
30	28, 16, 29	co 3948	. . . . . . . 8 class ((abs` y) x. (n` x))
31	26, 30	wceq 953	. . . . . . 7 wff (n` (ysx)) = ((abs` y) x. (n` x))
32		cc 5204	. . . . . . 7 class CC
33	31, 23, 32	wral 1637	. . . . . 6 wff A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x))
34	15, 24, 3	co 3948	. . . . . . . . 9 class (xgy)
35	34, 12	cfv 3172	. . . . . . . 8 class (n` (xgy))
36	24, 12	cfv 3172	. . . . . . . . 9 class (n` y)
37		caddc 5209	. . . . . . . . 9 class +
38	16, 36, 37	co 3948	. . . . . . . 8 class ((n` x) + (n` y))
39		cle 5267	. . . . . . . 8 class <_
40	35, 38, 39	wbr 2609	. . . . . . 7 wff (n` (xgy)) <_ ((n` x) + (n` y))
41	40, 23, 9	wral 1637	. . . . . 6 wff A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))
42	22, 33, 41	w3a 773	. . . . 5 wff (((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)))
43	42, 14, 9	wral 1637	. . . 4 wff A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y)))
44	8, 13, 43	w3a 773	. . 3 wff (<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))))
45	44, 2, 4, 11	copab2 3949	. 2 class {<.<.g, s>., n>. | (<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))))}
46	1, 45	wceq 953	1 wff NrmCVec = {<.<.g, s>., n>. | (<.g, s>. e. CVec /\ n:ran g-->RR /\ A.x e. ran g(((n` x) = 0 -> x = (Id` g)) /\ A.y e. CC (n` (ysx)) = ((abs` y) x. (n` x)) /\ A.y e. ran g(n` (xgy)) <_ ((n` x) + (n` y))))}

This definition is referenced by:  nvss 8150  nvvcop 8151  isnvlem 8167  isnvgOLD 8168  nvi 8173

Copyright terms: Public domain