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 = 1 st W
vciOLD.2 S = 2 nd W
vciOLD.3 X = ran G
Assertion vciOLD W CVec OLD G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x

Proof

Step Hyp Ref Expression
1 vciOLD.1 G = 1 st W
2 vciOLD.2 S = 2 nd W
3 vciOLD.3 X = ran G
4 1 eqeq2i g = G g = 1 st 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 x g z = x G z
14 13 oveq2d g = G y s x g z = y s x G z
15 oveq g = G y s x g y s z = y s x G y s z
16 14 15 eqeq12d g = G y s x g z = y s x g y s z y s x G z = y s x G y s z
17 7 16 raleqbidv g = G z ran g y s x g z = y s x g y s z z X y s x G z = y s x G y s z
18 oveq g = G y s x g z s x = y s x G z s x
19 18 eqeq2d g = G y + z s x = y s x g z s x y + z s x = y s x G z s x
20 19 anbi1d g = G y + z s x = y s x g z s x y z s x = y s z s x y + z s x = y s x G z s x y z s x = y s z s x
21 20 ralbidv g = G z y + z s x = y s x g z s x y z s x = y s z s x z y + z s x = y s x G z s x y z s x = y s z s x
22 17 21 anbi12d g = G z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x
23 22 ralbidv g = G y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x
24 23 anbi2d g = G 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x
25 7 24 raleqbidv g = G x ran g 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x x X 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x
26 5 12 25 3anbi123d g = G g AbelOp s : × ran g ran g x ran g 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x G AbelOp s : × X X x X 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x
27 4 26 sylbir g = 1 st W g AbelOp s : × ran g ran g x ran g 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x G AbelOp s : × X X x X 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x
28 2 eqeq2i s = S s = 2 nd W
29 feq1 s = S s : × X X S : × X X
30 oveq s = S 1 s x = 1 S x
31 30 eqeq1d s = S 1 s x = x 1 S x = x
32 oveq s = S y s x G z = y S x G z
33 oveq s = S y s x = y S x
34 oveq s = S y s z = y S z
35 33 34 oveq12d s = S y s x G y s z = y S x G y S z
36 32 35 eqeq12d s = S y s x G z = y s x G y s z y S x G z = y S x G y S z
37 36 ralbidv s = S z X y s x G z = y s x G y s z z X y S x G z = y S x G y S z
38 oveq s = S y + z s x = y + z S x
39 oveq s = S z s x = z S x
40 33 39 oveq12d s = S y s x G z s x = y S x G z S x
41 38 40 eqeq12d s = S y + z s x = y s x G z s x y + z S x = y S x G z S x
42 oveq s = S y z s x = y z S x
43 39 oveq2d s = S y s z s x = y s z S x
44 oveq s = S y s z S x = y S z S x
45 43 44 eqtrd s = S y s z s x = y S z S x
46 42 45 eqeq12d s = S y z s x = y s z s x y z S x = y S z S x
47 41 46 anbi12d s = S y + z s x = y s x G z s x y z s x = y s z s x y + z S x = y S x G z S x y z S x = y S z S x
48 47 ralbidv s = S z y + z s x = y s x G z s x y z s x = y s z s x z y + z S x = y S x G z S x y z S x = y S z S x
49 37 48 anbi12d s = S z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
50 49 ralbidv s = S y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
51 31 50 anbi12d s = S 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
52 51 ralbidv s = S x X 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
53 29 52 3anbi23d s = S G AbelOp s : × X X x X 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
54 28 53 sylbir s = 2 nd W G AbelOp s : × X X x X 1 s x = x y z X y s x G z = y s x G y s z z y + z s x = y s x G z s x y z s x = y s z s x G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
55 27 54 elopabi W g s | g AbelOp s : × ran g ran g x ran g 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x
56 df-vc CVec OLD = g s | g AbelOp s : × ran g ran g x ran g 1 s x = x y z ran g y s x g z = y s x g y s z z y + z s x = y s x g z s x y z s x = y s z s x
57 55 56 eleq2s W CVec OLD G AbelOp S : × X X x X 1 S x = x y z X y S x G z = y S x G y S z z y + z S x = y S x G z S x y z S x = y S z S x