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 
|- G e. AbelOp
isvciOLD.2 
|- dom G = ( X X. X )
isvciOLD.3 
|- S : ( CC X. X ) --> X
isvciOLD.4 
|- ( x e. X -> ( 1 S x ) = x )
isvciOLD.5 
|- ( ( y e. CC /\ x e. X /\ z e. X ) -> ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
isvciOLD.6 
|- ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) )
isvciOLD.7 
|- ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
isvciOLD.8 
|- W = <. G , S >.
Assertion isvciOLD 
|- W e. CVecOLD

Proof

Step Hyp Ref Expression
1 isvciOLD.1 
 |-  G e. AbelOp
2 isvciOLD.2 
 |-  dom G = ( X X. X )
3 isvciOLD.3 
 |-  S : ( CC X. X ) --> X
4 isvciOLD.4 
 |-  ( x e. X -> ( 1 S x ) = x )
5 isvciOLD.5 
 |-  ( ( y e. CC /\ x e. X /\ z e. X ) -> ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
6 isvciOLD.6 
 |-  ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) )
7 isvciOLD.7 
 |-  ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( y x. z ) S x ) = ( y S ( z S x ) ) )
8 isvciOLD.8 
 |-  W = <. G , S >.
9 5 3com12 
 |-  ( ( x e. X /\ y e. CC /\ z e. X ) -> ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
10 9 3expa 
 |-  ( ( ( x e. X /\ y e. CC ) /\ z e. X ) -> ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
11 10 ralrimiva 
 |-  ( ( x e. X /\ y e. CC ) -> A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) )
12 6 7 jca 
 |-  ( ( y e. CC /\ z e. CC /\ x e. X ) -> ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) )
13 12 3comr 
 |-  ( ( x e. X /\ y e. CC /\ z e. CC ) -> ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) )
14 13 3expa 
 |-  ( ( ( x e. X /\ y e. CC ) /\ z e. CC ) -> ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) )
15 14 ralrimiva 
 |-  ( ( x e. X /\ y e. CC ) -> 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 ) ) ) )
16 11 15 jca 
 |-  ( ( x e. X /\ 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 ) ) ) ) )
17 16 ralrimiva 
 |-  ( x e. 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 ) ) ) ) )
18 4 17 jca 
 |-  ( 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 ) ) ) ) ) )
19 18 rgen 
 |-  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 ) ) ) ) )
20 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
21 1 20 ax-mp 
 |-  G e. GrpOp
22 21 2 grporn 
 |-  X = ran G
23 22 isvcOLD 
 |-  ( <. G , S >. 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 ) ) ) ) ) ) )
24 1 3 19 23 mpbir3an 
 |-  <. G , S >. e. CVecOLD
25 8 24 eqeltri 
 |-  W e. CVecOLD