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