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