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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cnv | |
|
1 | vg | |
|
2 | vs | |
|
3 | vn | |
|
4 | 1 | cv | |
5 | 2 | cv | |
6 | 4 5 | cop | |
7 | cvc | |
|
8 | 6 7 | wcel | |
9 | 3 | cv | |
10 | 4 | crn | |
11 | cr | |
|
12 | 10 11 9 | wf | |
13 | vx | |
|
14 | 13 | cv | |
15 | 14 9 | cfv | |
16 | cc0 | |
|
17 | 15 16 | wceq | |
18 | cgi | |
|
19 | 4 18 | cfv | |
20 | 14 19 | wceq | |
21 | 17 20 | wi | |
22 | vy | |
|
23 | cc | |
|
24 | 22 | cv | |
25 | 24 14 5 | co | |
26 | 25 9 | cfv | |
27 | cabs | |
|
28 | 24 27 | cfv | |
29 | cmul | |
|
30 | 28 15 29 | co | |
31 | 26 30 | wceq | |
32 | 31 22 23 | wral | |
33 | 14 24 4 | co | |
34 | 33 9 | cfv | |
35 | cle | |
|
36 | caddc | |
|
37 | 24 9 | cfv | |
38 | 15 37 36 | co | |
39 | 34 38 35 | wbr | |
40 | 39 22 10 | wral | |
41 | 21 32 40 | w3a | |
42 | 41 13 10 | wral | |
43 | 8 12 42 | w3a | |
44 | 43 1 2 3 | coprab | |
45 | 0 44 | wceq | |