Step |
Hyp |
Ref |
Expression |
1 |
|
vc0.1 |
|- G = ( 1st ` W ) |
2 |
|
vc0.2 |
|- S = ( 2nd ` W ) |
3 |
|
vc0.3 |
|- X = ran G |
4 |
|
vc0.4 |
|- Z = ( GId ` G ) |
5 |
1 3 4
|
vc0rid |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G Z ) = A ) |
6 |
|
1p0e1 |
|- ( 1 + 0 ) = 1 |
7 |
6
|
oveq1i |
|- ( ( 1 + 0 ) S A ) = ( 1 S A ) |
8 |
|
0cn |
|- 0 e. CC |
9 |
|
ax-1cn |
|- 1 e. CC |
10 |
1 2 3
|
vcdir |
|- ( ( W e. CVecOLD /\ ( 1 e. CC /\ 0 e. CC /\ A e. X ) ) -> ( ( 1 + 0 ) S A ) = ( ( 1 S A ) G ( 0 S A ) ) ) |
11 |
9 10
|
mp3anr1 |
|- ( ( W e. CVecOLD /\ ( 0 e. CC /\ A e. X ) ) -> ( ( 1 + 0 ) S A ) = ( ( 1 S A ) G ( 0 S A ) ) ) |
12 |
8 11
|
mpanr1 |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 + 0 ) S A ) = ( ( 1 S A ) G ( 0 S A ) ) ) |
13 |
1 2 3
|
vcidOLD |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A ) |
14 |
7 12 13
|
3eqtr3a |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 S A ) G ( 0 S A ) ) = A ) |
15 |
13
|
oveq1d |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 1 S A ) G ( 0 S A ) ) = ( A G ( 0 S A ) ) ) |
16 |
5 14 15
|
3eqtr2rd |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G ( 0 S A ) ) = ( A G Z ) ) |
17 |
1 2 3
|
vccl |
|- ( ( W e. CVecOLD /\ 0 e. CC /\ A e. X ) -> ( 0 S A ) e. X ) |
18 |
8 17
|
mp3an2 |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) e. X ) |
19 |
1 3 4
|
vczcl |
|- ( W e. CVecOLD -> Z e. X ) |
20 |
19
|
adantr |
|- ( ( W e. CVecOLD /\ A e. X ) -> Z e. X ) |
21 |
|
simpr |
|- ( ( W e. CVecOLD /\ A e. X ) -> A e. X ) |
22 |
18 20 21
|
3jca |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( 0 S A ) e. X /\ Z e. X /\ A e. X ) ) |
23 |
1 3
|
vclcan |
|- ( ( W e. CVecOLD /\ ( ( 0 S A ) e. X /\ Z e. X /\ A e. X ) ) -> ( ( A G ( 0 S A ) ) = ( A G Z ) <-> ( 0 S A ) = Z ) ) |
24 |
22 23
|
syldan |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( ( A G ( 0 S A ) ) = ( A G Z ) <-> ( 0 S A ) = Z ) ) |
25 |
16 24
|
mpbid |
|- ( ( W e. CVecOLD /\ A e. X ) -> ( 0 S A ) = Z ) |