Description: Properties that determine a complex vector space. (Contributed by NM, 5-Nov-2006) Obsolete version of iscvsi . (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isvciOLD.1 | |
|
isvciOLD.2 | |
||
isvciOLD.3 | |
||
isvciOLD.4 | |
||
isvciOLD.5 | |
||
isvciOLD.6 | |
||
isvciOLD.7 | |
||
isvciOLD.8 | |
||
Assertion | isvciOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isvciOLD.1 | |
|
2 | isvciOLD.2 | |
|
3 | isvciOLD.3 | |
|
4 | isvciOLD.4 | |
|
5 | isvciOLD.5 | |
|
6 | isvciOLD.6 | |
|
7 | isvciOLD.7 | |
|
8 | isvciOLD.8 | |
|
9 | 5 | 3com12 | |
10 | 9 | 3expa | |
11 | 10 | ralrimiva | |
12 | 6 7 | jca | |
13 | 12 | 3comr | |
14 | 13 | 3expa | |
15 | 14 | ralrimiva | |
16 | 11 15 | jca | |
17 | 16 | ralrimiva | |
18 | 4 17 | jca | |
19 | 18 | rgen | |
20 | ablogrpo | |
|
21 | 1 20 | ax-mp | |
22 | 21 2 | grporn | |
23 | 22 | isvcOLD | |
24 | 1 3 19 23 | mpbir3an | |
25 | 8 24 | eqeltri | |