Step |
Hyp |
Ref |
Expression |
1 |
|
nvmdi.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvmdi.3 |
|- M = ( -v ` U ) |
3 |
|
nvmdi.4 |
|- S = ( .sOLD ` U ) |
4 |
|
simpr1 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> A e. CC ) |
5 |
|
simpr2 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> B e. X ) |
6 |
|
neg1cn |
|- -u 1 e. CC |
7 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ C e. X ) -> ( -u 1 S C ) e. X ) |
8 |
6 7
|
mp3an2 |
|- ( ( U e. NrmCVec /\ C e. X ) -> ( -u 1 S C ) e. X ) |
9 |
8
|
3ad2antr3 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( -u 1 S C ) e. X ) |
10 |
4 5 9
|
3jca |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A e. CC /\ B e. X /\ ( -u 1 S C ) e. X ) ) |
11 |
|
eqid |
|- ( +v ` U ) = ( +v ` U ) |
12 |
1 11 3
|
nvdi |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ ( -u 1 S C ) e. X ) ) -> ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( A S ( -u 1 S C ) ) ) ) |
13 |
10 12
|
syldan |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( A S ( -u 1 S C ) ) ) ) |
14 |
1 3
|
nvscom |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ -u 1 e. CC /\ C e. X ) ) -> ( A S ( -u 1 S C ) ) = ( -u 1 S ( A S C ) ) ) |
15 |
6 14
|
mp3anr2 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ C e. X ) ) -> ( A S ( -u 1 S C ) ) = ( -u 1 S ( A S C ) ) ) |
16 |
15
|
3adantr2 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( -u 1 S C ) ) = ( -u 1 S ( A S C ) ) ) |
17 |
16
|
oveq2d |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( ( A S B ) ( +v ` U ) ( A S ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) ) |
18 |
13 17
|
eqtrd |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) ) |
19 |
1 11 3 2
|
nvmval |
|- ( ( U e. NrmCVec /\ B e. X /\ C e. X ) -> ( B M C ) = ( B ( +v ` U ) ( -u 1 S C ) ) ) |
20 |
19
|
3adant3r1 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( B M C ) = ( B ( +v ` U ) ( -u 1 S C ) ) ) |
21 |
20
|
oveq2d |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B M C ) ) = ( A S ( B ( +v ` U ) ( -u 1 S C ) ) ) ) |
22 |
|
simpl |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> U e. NrmCVec ) |
23 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A S B ) e. X ) |
24 |
23
|
3adant3r3 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S B ) e. X ) |
25 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ A e. CC /\ C e. X ) -> ( A S C ) e. X ) |
26 |
25
|
3adant3r2 |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S C ) e. X ) |
27 |
1 11 3 2
|
nvmval |
|- ( ( U e. NrmCVec /\ ( A S B ) e. X /\ ( A S C ) e. X ) -> ( ( A S B ) M ( A S C ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) ) |
28 |
22 24 26 27
|
syl3anc |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( ( A S B ) M ( A S C ) ) = ( ( A S B ) ( +v ` U ) ( -u 1 S ( A S C ) ) ) ) |
29 |
18 21 28
|
3eqtr4d |
|- ( ( U e. NrmCVec /\ ( A e. CC /\ B e. X /\ C e. X ) ) -> ( A S ( B M C ) ) = ( ( A S B ) M ( A S C ) ) ) |