Step |
Hyp |
Ref |
Expression |
1 |
|
nvdif.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvdif.2 |
|- G = ( +v ` U ) |
3 |
|
nvdif.4 |
|- S = ( .sOLD ` U ) |
4 |
|
nvdif.6 |
|- N = ( normCV ` U ) |
5 |
|
simp1 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> U e. NrmCVec ) |
6 |
|
neg1cn |
|- -u 1 e. CC |
7 |
6
|
a1i |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> -u 1 e. CC ) |
8 |
|
simp3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> B e. X ) |
9 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ A e. X ) -> ( -u 1 S A ) e. X ) |
10 |
6 9
|
mp3an2 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S A ) e. X ) |
11 |
10
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S A ) e. X ) |
12 |
1 2 3
|
nvdi |
|- ( ( U e. NrmCVec /\ ( -u 1 e. CC /\ B e. X /\ ( -u 1 S A ) e. X ) ) -> ( -u 1 S ( B G ( -u 1 S A ) ) ) = ( ( -u 1 S B ) G ( -u 1 S ( -u 1 S A ) ) ) ) |
13 |
5 7 8 11 12
|
syl13anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S ( B G ( -u 1 S A ) ) ) = ( ( -u 1 S B ) G ( -u 1 S ( -u 1 S A ) ) ) ) |
14 |
1 3
|
nvnegneg |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( -u 1 S ( -u 1 S A ) ) = A ) |
15 |
14
|
3adant3 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S ( -u 1 S A ) ) = A ) |
16 |
15
|
oveq2d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( -u 1 S B ) G ( -u 1 S ( -u 1 S A ) ) ) = ( ( -u 1 S B ) G A ) ) |
17 |
1 3
|
nvscl |
|- ( ( U e. NrmCVec /\ -u 1 e. CC /\ B e. X ) -> ( -u 1 S B ) e. X ) |
18 |
6 17
|
mp3an2 |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( -u 1 S B ) e. X ) |
19 |
18
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S B ) e. X ) |
20 |
|
simp2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> A e. X ) |
21 |
1 2
|
nvcom |
|- ( ( U e. NrmCVec /\ ( -u 1 S B ) e. X /\ A e. X ) -> ( ( -u 1 S B ) G A ) = ( A G ( -u 1 S B ) ) ) |
22 |
5 19 20 21
|
syl3anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( -u 1 S B ) G A ) = ( A G ( -u 1 S B ) ) ) |
23 |
13 16 22
|
3eqtrd |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( -u 1 S ( B G ( -u 1 S A ) ) ) = ( A G ( -u 1 S B ) ) ) |
24 |
23
|
fveq2d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( -u 1 S ( B G ( -u 1 S A ) ) ) ) = ( N ` ( A G ( -u 1 S B ) ) ) ) |
25 |
1 2
|
nvgcl |
|- ( ( U e. NrmCVec /\ B e. X /\ ( -u 1 S A ) e. X ) -> ( B G ( -u 1 S A ) ) e. X ) |
26 |
5 8 11 25
|
syl3anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( B G ( -u 1 S A ) ) e. X ) |
27 |
1 3 4
|
nvm1 |
|- ( ( U e. NrmCVec /\ ( B G ( -u 1 S A ) ) e. X ) -> ( N ` ( -u 1 S ( B G ( -u 1 S A ) ) ) ) = ( N ` ( B G ( -u 1 S A ) ) ) ) |
28 |
5 26 27
|
syl2anc |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( -u 1 S ( B G ( -u 1 S A ) ) ) ) = ( N ` ( B G ( -u 1 S A ) ) ) ) |
29 |
24 28
|
eqtr3d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( N ` ( A G ( -u 1 S B ) ) ) = ( N ` ( B G ( -u 1 S A ) ) ) ) |