Metamath Proof Explorer


Theorem isvciOLD

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 GAbelOp
isvciOLD.2 domG=X×X
isvciOLD.3 S:×XX
isvciOLD.4 xX1Sx=x
isvciOLD.5 yxXzXySxGz=ySxGySz
isvciOLD.6 yzxXy+zSx=ySxGzSx
isvciOLD.7 yzxXyzSx=ySzSx
isvciOLD.8 W=GS
Assertion isvciOLD WCVecOLD

Proof

Step Hyp Ref Expression
1 isvciOLD.1 GAbelOp
2 isvciOLD.2 domG=X×X
3 isvciOLD.3 S:×XX
4 isvciOLD.4 xX1Sx=x
5 isvciOLD.5 yxXzXySxGz=ySxGySz
6 isvciOLD.6 yzxXy+zSx=ySxGzSx
7 isvciOLD.7 yzxXyzSx=ySzSx
8 isvciOLD.8 W=GS
9 5 3com12 xXyzXySxGz=ySxGySz
10 9 3expa xXyzXySxGz=ySxGySz
11 10 ralrimiva xXyzXySxGz=ySxGySz
12 6 7 jca yzxXy+zSx=ySxGzSxyzSx=ySzSx
13 12 3comr xXyzy+zSx=ySxGzSxyzSx=ySzSx
14 13 3expa xXyzy+zSx=ySxGzSxyzSx=ySzSx
15 14 ralrimiva xXyzy+zSx=ySxGzSxyzSx=ySzSx
16 11 15 jca xXyzXySxGz=ySxGySzzy+zSx=ySxGzSxyzSx=ySzSx
17 16 ralrimiva xXyzXySxGz=ySxGySzzy+zSx=ySxGzSxyzSx=ySzSx
18 4 17 jca xX1Sx=xyzXySxGz=ySxGySzzy+zSx=ySxGzSxyzSx=ySzSx
19 18 rgen xX1Sx=xyzXySxGz=ySxGySzzy+zSx=ySxGzSxyzSx=ySzSx
20 ablogrpo GAbelOpGGrpOp
21 1 20 ax-mp GGrpOp
22 21 2 grporn X=ranG
23 22 isvcOLD GSCVecOLDGAbelOpS:×XXxX1Sx=xyzXySxGz=ySxGySzzy+zSx=ySxGzSxyzSx=ySzSx
24 1 3 19 23 mpbir3an GSCVecOLD
25 8 24 eqeltri WCVecOLD