Step |
Hyp |
Ref |
Expression |
1 |
|
nvsz.4 |
|- S = ( .sOLD ` U ) |
2 |
|
nvsz.6 |
|- Z = ( 0vec ` U ) |
3 |
|
eqid |
|- ( 1st ` U ) = ( 1st ` U ) |
4 |
3
|
nvvc |
|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD ) |
5 |
|
eqid |
|- ( +v ` U ) = ( +v ` U ) |
6 |
5
|
vafval |
|- ( +v ` U ) = ( 1st ` ( 1st ` U ) ) |
7 |
1
|
smfval |
|- S = ( 2nd ` ( 1st ` U ) ) |
8 |
|
eqid |
|- ( BaseSet ` U ) = ( BaseSet ` U ) |
9 |
8 5
|
bafval |
|- ( BaseSet ` U ) = ran ( +v ` U ) |
10 |
|
eqid |
|- ( GId ` ( +v ` U ) ) = ( GId ` ( +v ` U ) ) |
11 |
6 7 9 10
|
vcz |
|- ( ( ( 1st ` U ) e. CVecOLD /\ A e. CC ) -> ( A S ( GId ` ( +v ` U ) ) ) = ( GId ` ( +v ` U ) ) ) |
12 |
4 11
|
sylan |
|- ( ( U e. NrmCVec /\ A e. CC ) -> ( A S ( GId ` ( +v ` U ) ) ) = ( GId ` ( +v ` U ) ) ) |
13 |
5 2
|
0vfval |
|- ( U e. NrmCVec -> Z = ( GId ` ( +v ` U ) ) ) |
14 |
13
|
adantr |
|- ( ( U e. NrmCVec /\ A e. CC ) -> Z = ( GId ` ( +v ` U ) ) ) |
15 |
14
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. CC ) -> ( A S Z ) = ( A S ( GId ` ( +v ` U ) ) ) ) |
16 |
12 15 14
|
3eqtr4d |
|- ( ( U e. NrmCVec /\ A e. CC ) -> ( A S Z ) = Z ) |