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 ) ) ) ) ) ) )