Step |
Hyp |
Ref |
Expression |
1 |
|
nvdi.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvdi.2 |
|- G = ( +v ` U ) |
3 |
|
nvdi.4 |
|- S = ( .sOLD ` U ) |
4 |
|
eqid |
|- ( 1st ` U ) = ( 1st ` U ) |
5 |
4
|
nvvc |
|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD ) |
6 |
2
|
vafval |
|- G = ( 1st ` ( 1st ` U ) ) |
7 |
3
|
smfval |
|- S = ( 2nd ` ( 1st ` U ) ) |
8 |
1 2
|
bafval |
|- X = ran G |
9 |
6 7 8
|
vcdir |
|- ( ( ( 1st ` U ) e. CVecOLD /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) ) |
10 |
5 9
|
sylan |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. CC /\ C e. X ) ) -> ( ( A + B ) S C ) = ( ( A S C ) G ( B S C ) ) ) |