Metamath Proof Explorer


Definition df-nv

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

Ref Expression
Assertion df-nv NrmCVec=gsn|gsCVecOLDn:rangxrangnx=0x=GIdgynysx=ynxyrangnxgynx+ny

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnv classNrmCVec
1 vg setvarg
2 vs setvars
3 vn setvarn
4 1 cv setvarg
5 2 cv setvars
6 4 5 cop classgs
7 cvc classCVecOLD
8 6 7 wcel wffgsCVecOLD
9 3 cv setvarn
10 4 crn classrang
11 cr class
12 10 11 9 wf wffn:rang
13 vx setvarx
14 13 cv setvarx
15 14 9 cfv classnx
16 cc0 class0
17 15 16 wceq wffnx=0
18 cgi classGId
19 4 18 cfv classGIdg
20 14 19 wceq wffx=GIdg
21 17 20 wi wffnx=0x=GIdg
22 vy setvary
23 cc class
24 22 cv setvary
25 24 14 5 co classysx
26 25 9 cfv classnysx
27 cabs classabs
28 24 27 cfv classy
29 cmul class×
30 28 15 29 co classynx
31 26 30 wceq wffnysx=ynx
32 31 22 23 wral wffynysx=ynx
33 14 24 4 co classxgy
34 33 9 cfv classnxgy
35 cle class
36 caddc class+
37 24 9 cfv classny
38 15 37 36 co classnx+ny
39 34 38 35 wbr wffnxgynx+ny
40 39 22 10 wral wffyrangnxgynx+ny
41 21 32 40 w3a wffnx=0x=GIdgynysx=ynxyrangnxgynx+ny
42 41 13 10 wral wffxrangnx=0x=GIdgynysx=ynxyrangnxgynx+ny
43 8 12 42 w3a wffgsCVecOLDn:rangxrangnx=0x=GIdgynysx=ynxyrangnxgynx+ny
44 43 1 2 3 coprab classgsn|gsCVecOLDn:rangxrangnx=0x=GIdgynysx=ynxyrangnxgynx+ny
45 0 44 wceq wffNrmCVec=gsn|gsCVecOLDn:rangxrangnx=0x=GIdgynysx=ynxyrangnxgynx+ny