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
|
vczcl |
|- ( W e. CVecOLD -> Z e. X ) |
6 |
5
|
anim2i |
|- ( ( A e. CC /\ W e. CVecOLD ) -> ( A e. CC /\ Z e. X ) ) |
7 |
6
|
ancoms |
|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A e. CC /\ Z e. X ) ) |
8 |
|
0cn |
|- 0 e. CC |
9 |
1 2 3
|
vcass |
|- ( ( W e. CVecOLD /\ ( A e. CC /\ 0 e. CC /\ Z e. X ) ) -> ( ( A x. 0 ) S Z ) = ( A S ( 0 S Z ) ) ) |
10 |
8 9
|
mp3anr2 |
|- ( ( W e. CVecOLD /\ ( A e. CC /\ Z e. X ) ) -> ( ( A x. 0 ) S Z ) = ( A S ( 0 S Z ) ) ) |
11 |
7 10
|
syldan |
|- ( ( W e. CVecOLD /\ A e. CC ) -> ( ( A x. 0 ) S Z ) = ( A S ( 0 S Z ) ) ) |
12 |
|
mul01 |
|- ( A e. CC -> ( A x. 0 ) = 0 ) |
13 |
12
|
oveq1d |
|- ( A e. CC -> ( ( A x. 0 ) S Z ) = ( 0 S Z ) ) |
14 |
1 2 3 4
|
vc0 |
|- ( ( W e. CVecOLD /\ Z e. X ) -> ( 0 S Z ) = Z ) |
15 |
5 14
|
mpdan |
|- ( W e. CVecOLD -> ( 0 S Z ) = Z ) |
16 |
13 15
|
sylan9eqr |
|- ( ( W e. CVecOLD /\ A e. CC ) -> ( ( A x. 0 ) S Z ) = Z ) |
17 |
15
|
oveq2d |
|- ( W e. CVecOLD -> ( A S ( 0 S Z ) ) = ( A S Z ) ) |
18 |
17
|
adantr |
|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A S ( 0 S Z ) ) = ( A S Z ) ) |
19 |
11 16 18
|
3eqtr3rd |
|- ( ( W e. CVecOLD /\ A e. CC ) -> ( A S Z ) = Z ) |