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 e. CVecOLD -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )

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 e. AbelOp <-> G e. AbelOp ) )
6 rneq 
 |-  ( g = G -> ran g = ran G )
7 6 3 eqtr4di 
 |-  ( g = G -> ran g = X )
8 xpeq2 
 |-  ( ran g = X -> ( CC X. ran g ) = ( CC X. X ) )
9 8 feq2d 
 |-  ( ran g = X -> ( s : ( CC X. ran g ) --> ran g <-> s : ( CC X. X ) --> ran g ) )
10 feq3 
 |-  ( ran g = X -> ( s : ( CC X. X ) --> ran g <-> s : ( CC X. X ) --> X ) )
11 9 10 bitrd 
 |-  ( ran g = X -> ( s : ( CC X. ran g ) --> ran g <-> s : ( CC X. X ) --> X ) )
12 7 11 syl 
 |-  ( g = G -> ( s : ( CC X. ran g ) --> ran g <-> s : ( CC X. 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 -> ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) <-> A. z e. 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 x. z ) s x ) = ( y s ( z s x ) ) ) <-> ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) )
21 20 ralbidv 
 |-  ( g = G -> ( A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) <-> A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) )
22 17 21 anbi12d 
 |-  ( g = G -> ( ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) )
23 22 ralbidv 
 |-  ( g = G -> ( A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) )
24 23 anbi2d 
 |-  ( g = G -> ( ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) )
25 7 24 raleqbidv 
 |-  ( g = G -> ( A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) )
26 5 12 25 3anbi123d 
 |-  ( g = G -> ( ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) <-> ( G e. AbelOp /\ s : ( CC X. X ) --> X /\ A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) ) )
27 4 26 sylbir 
 |-  ( g = ( 1st ` W ) -> ( ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) <-> ( G e. AbelOp /\ s : ( CC X. X ) --> X /\ A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) ) )
28 2 eqeq2i 
 |-  ( s = S <-> s = ( 2nd ` W ) )
29 feq1 
 |-  ( s = S -> ( s : ( CC X. X ) --> X <-> S : ( CC X. 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 -> ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) <-> A. z e. 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 x. z ) s x ) = ( ( y x. 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 x. z ) s x ) = ( y s ( z s x ) ) <-> ( ( y x. 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 x. z ) s x ) = ( y s ( z s x ) ) ) <-> ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) )
48 47 ralbidv 
 |-  ( s = S -> ( A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) <-> A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) )
49 37 48 anbi12d 
 |-  ( s = S -> ( ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) )
50 49 ralbidv 
 |-  ( s = S -> ( A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) <-> A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) )
51 31 50 anbi12d 
 |-  ( s = S -> ( ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
52 51 ralbidv 
 |-  ( s = S -> ( A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) <-> A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
53 29 52 3anbi23d 
 |-  ( s = S -> ( ( G e. AbelOp /\ s : ( CC X. X ) --> X /\ A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )
54 28 53 sylbir 
 |-  ( s = ( 2nd ` W ) -> ( ( G e. AbelOp /\ s : ( CC X. X ) --> X /\ A. x e. X ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. X ( y s ( x G z ) ) = ( ( y s x ) G ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) G ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) <-> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) ) )
55 27 54 elopabi 
 |-  ( W e. { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) } -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
56 df-vc 
 |-  CVecOLD = { <. g , s >. | ( g e. AbelOp /\ s : ( CC X. ran g ) --> ran g /\ A. x e. ran g ( ( 1 s x ) = x /\ A. y e. CC ( A. z e. ran g ( y s ( x g z ) ) = ( ( y s x ) g ( y s z ) ) /\ A. z e. CC ( ( ( y + z ) s x ) = ( ( y s x ) g ( z s x ) ) /\ ( ( y x. z ) s x ) = ( y s ( z s x ) ) ) ) ) ) }
57 55 56 eleq2s 
 |-  ( W e. CVecOLD -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )