This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isvcOLD

Description: The predicate "is a complex vector space." (Contributed by NM, 31-May-2008) Obsolete version of iscvsp . (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis isvcOLD.1 
|- X = ran G
Assertion 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 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isvcOLD.1 
 |-  X = ran G
2 vcex 
 |-  ( <. G , S >. e. CVecOLD -> ( G e. _V /\ S e. _V ) )
3 elex 
 |-  ( G e. AbelOp -> G e. _V )
4 3 adantr 
 |-  ( ( G e. AbelOp /\ S : ( CC X. X ) --> X ) -> G e. _V )
5 cnex 
 |-  CC e. _V
6 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
7 rnexg 
 |-  ( G e. GrpOp -> ran G e. _V )
8 1 7 eqeltrid 
 |-  ( G e. GrpOp -> X e. _V )
9 6 8 syl 
 |-  ( G e. AbelOp -> X e. _V )
10 xpexg 
 |-  ( ( CC e. _V /\ X e. _V ) -> ( CC X. X ) e. _V )
11 5 9 10 sylancr 
 |-  ( G e. AbelOp -> ( CC X. X ) e. _V )
12 fex 
 |-  ( ( S : ( CC X. X ) --> X /\ ( CC X. X ) e. _V ) -> S e. _V )
13 11 12 sylan2 
 |-  ( ( S : ( CC X. X ) --> X /\ G e. AbelOp ) -> S e. _V )
14 13 ancoms 
 |-  ( ( G e. AbelOp /\ S : ( CC X. X ) --> X ) -> S e. _V )
15 4 14 jca 
 |-  ( ( G e. AbelOp /\ S : ( CC X. X ) --> X ) -> ( G e. _V /\ S e. _V ) )
16 15 3adant3 
 |-  ( ( 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. _V /\ S e. _V ) )
17 1 isvclem 
 |-  ( ( G e. _V /\ S e. _V ) -> ( <. 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 ) ) ) ) ) ) ) )
18 2 16 17 pm5.21nii 
 |-  ( <. 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 ) ) ) ) ) ) )