Step |
Hyp |
Ref |
Expression |
1 |
|
nvmval.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvmval.2 |
|- G = ( +v ` U ) |
3 |
|
nvmval.4 |
|- S = ( .sOLD ` U ) |
4 |
|
nvmval.3 |
|- M = ( -v ` U ) |
5 |
1 2 3 4
|
nvmval |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( A G ( -u 1 S B ) ) ) |
6 |
|
neg1cn |
|- -u 1 e. CC |
7 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X ) |
8 |
6 7
|
mp3an2 |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) e. X ) |
9 |
8
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) e. X ) |
10 |
1 2
|
nvcom |
|- ( ( U e. NrmCVec /\ A e. X /\ ( -u 1 S B ) e. X ) -> ( A G ( -u 1 S B ) ) = ( ( -u 1 S B ) G A ) ) |
11 |
9 10
|
syld3an3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A G ( -u 1 S B ) ) = ( ( -u 1 S B ) G A ) ) |
12 |
5 11
|
eqtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) = ( ( -u 1 S B ) G A ) ) |