Step |
Hyp |
Ref |
Expression |
1 |
|
vciOLD.1 |
|- G = ( 1st ` W ) |
2 |
|
vciOLD.2 |
|- S = ( 2nd ` W ) |
3 |
|
vciOLD.3 |
|- X = ran G |
4 |
1 2 3
|
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 ) ) ) ) ) ) ) |
5 |
|
simpl |
|- ( ( ( 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 ) |
6 |
5
|
ralimi |
|- ( 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 ) |
7 |
6
|
3ad2ant3 |
|- ( ( 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 ) ) ) ) ) ) -> A. x e. X ( 1 S x ) = x ) |
8 |
4 7
|
syl |
|- ( W e. CVecOLD -> A. x e. X ( 1 S x ) = x ) |
9 |
|
oveq2 |
|- ( x = A -> ( 1 S x ) = ( 1 S A ) ) |
10 |
|
id |
|- ( x = A -> x = A ) |
11 |
9 10
|
eqeq12d |
|- ( x = A -> ( ( 1 S x ) = x <-> ( 1 S A ) = A ) ) |
12 |
11
|
rspccva |
|- ( ( A. x e. X ( 1 S x ) = x /\ A e. X ) -> ( 1 S A ) = A ) |
13 |
8 12
|
sylan |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A ) |