Metamath Proof Explorer

Theorem vciOLD

Description: Obsolete version of cvsi . The properties of a complex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. The variable W was chosen because _V is already used for the universal class. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses vciOLD.1 ⊢G=1st⁡W
vciOLD.2 ⊢S=2nd⁡W
vciOLD.3 ⊢X=ran⁡G
Assertion vciOLD ⊢W∈CVecOLD→G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx

Proof

Step Hyp Ref Expression
1 vciOLD.1 ⊢G=1st⁡W
2 vciOLD.2 ⊢S=2nd⁡W
3 vciOLD.3 ⊢X=ran⁡G
4 1 eqeq2i ⊢g=G↔g=1st⁡W
5 eleq1 ⊢g=G→g∈AbelOp↔G∈AbelOp
6 rneq ⊢g=G→ran⁡g=ran⁡G
7 6 3 eqtr4di ⊢g=G→ran⁡g=X
8 xpeq2 ⊢ran⁡g=X→ℂ×ran⁡g=ℂ×X
9 8 feq2d ⊢ran⁡g=X→s:ℂ×ran⁡g⟶ran⁡g↔s:ℂ×X⟶ran⁡g
10 feq3 ⊢ran⁡g=X→s:ℂ×X⟶ran⁡g↔s:ℂ×X⟶X
11 9 10 bitrd ⊢ran⁡g=X→s:ℂ×ran⁡g⟶ran⁡g↔s:ℂ×X⟶X
12 7 11 syl ⊢g=G→s:ℂ×ran⁡g⟶ran⁡g↔s:ℂ×X⟶X
13 oveq ⊢g=G→xgz=xGz
14 13 oveq2d ⊢g=G→ysxgz=ysxGz
15 oveq ⊢g=G→ysxgysz=ysxGysz
16 14 15 eqeq12d ⊢g=G→ysxgz=ysxgysz↔ysxGz=ysxGysz
17 7 16 raleqbidv ⊢g=G→∀z∈ran⁡gysxgz=ysxgysz↔∀z∈XysxGz=ysxGysz
18 oveq ⊢g=G→ysxgzsx=ysxGzsx
19 18 eqeq2d ⊢g=G→y+zsx=ysxgzsx↔y+zsx=ysxGzsx
20 19 anbi1d ⊢g=G→y+zsx=ysxgzsx∧y⁢zsx=yszsx↔y+zsx=ysxGzsx∧y⁢zsx=yszsx
21 20 ralbidv ⊢g=G→∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
22 17 21 anbi12d ⊢g=G→∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
23 22 ralbidv ⊢g=G→∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
24 23 anbi2d ⊢g=G→1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
25 7 24 raleqbidv ⊢g=G→∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
26 5 12 25 3anbi123d ⊢g=G→g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔G∈AbelOp∧s:ℂ×X⟶X∧∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
27 4 26 sylbir ⊢g=1st⁡W→g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx↔G∈AbelOp∧s:ℂ×X⟶X∧∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx
28 2 eqeq2i ⊢s=S↔s=2nd⁡W
29 feq1 ⊢s=S→s:ℂ×X⟶X↔S:ℂ×X⟶X
30 oveq ⊢s=S→1sx=1Sx
31 30 eqeq1d ⊢s=S→1sx=x↔1Sx=x
32 oveq ⊢s=S→ysxGz=ySxGz
33 oveq ⊢s=S→ysx=ySx
34 oveq ⊢s=S→ysz=ySz
35 33 34 oveq12d ⊢s=S→ysxGysz=ySxGySz
36 32 35 eqeq12d ⊢s=S→ysxGz=ysxGysz↔ySxGz=ySxGySz
37 36 ralbidv ⊢s=S→∀z∈XysxGz=ysxGysz↔∀z∈XySxGz=ySxGySz
38 oveq ⊢s=S→y+zsx=y+zSx
39 oveq ⊢s=S→zsx=zSx
40 33 39 oveq12d ⊢s=S→ysxGzsx=ySxGzSx
41 38 40 eqeq12d ⊢s=S→y+zsx=ysxGzsx↔y+zSx=ySxGzSx
42 oveq ⊢s=S→y⁢zsx=y⁢zSx
43 39 oveq2d ⊢s=S→yszsx=yszSx
44 oveq ⊢s=S→yszSx=ySzSx
45 43 44 eqtrd ⊢s=S→yszsx=ySzSx
46 42 45 eqeq12d ⊢s=S→y⁢zsx=yszsx↔y⁢zSx=ySzSx
47 41 46 anbi12d ⊢s=S→y+zsx=ysxGzsx∧y⁢zsx=yszsx↔y+zSx=ySxGzSx∧y⁢zSx=ySzSx
48 47 ralbidv ⊢s=S→∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
49 37 48 anbi12d ⊢s=S→∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
50 49 ralbidv ⊢s=S→∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
51 31 50 anbi12d ⊢s=S→1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
52 51 ralbidv ⊢s=S→∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
53 29 52 3anbi23d ⊢s=S→G∈AbelOp∧s:ℂ×X⟶X∧∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
54 28 53 sylbir ⊢s=2nd⁡W→G∈AbelOp∧s:ℂ×X⟶X∧∀x∈X1sx=x∧∀y∈ℂ∀z∈XysxGz=ysxGysz∧∀z∈ℂy+zsx=ysxGzsx∧y⁢zsx=yszsx↔G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
55 27 54 elopabi ⊢W∈gs|g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx→G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx
56 df-vc ⊢CVecOLD=gs|g∈AbelOp∧s:ℂ×ran⁡g⟶ran⁡g∧∀x∈ran⁡g1sx=x∧∀y∈ℂ∀z∈ran⁡gysxgz=ysxgysz∧∀z∈ℂy+zsx=ysxgzsx∧y⁢zsx=yszsx
57 55 56 eleq2s ⊢W∈CVecOLD→G∈AbelOp∧S:ℂ×X⟶X∧∀x∈X1Sx=x∧∀y∈ℂ∀z∈XySxGz=ySxGySz∧∀z∈ℂy+zSx=ySxGzSx∧y⁢zSx=ySzSx