Step |
Hyp |
Ref |
Expression |
1 |
|
nvnd.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvnd.5 |
|- Z = ( 0vec ` U ) |
3 |
|
nvnd.6 |
|- N = ( normCV ` U ) |
4 |
|
nvnd.8 |
|- D = ( IndMet ` U ) |
5 |
1 2
|
nvzcl |
|- ( U e. NrmCVec -> Z e. X ) |
6 |
5
|
adantr |
|- ( ( U e. NrmCVec /\ A e. X ) -> Z e. X ) |
7 |
|
eqid |
|- ( -v ` U ) = ( -v ` U ) |
8 |
1 7 3 4
|
imsdval |
|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( A D Z ) = ( N ` ( A ( -v ` U ) Z ) ) ) |
9 |
6 8
|
mpd3an3 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A D Z ) = ( N ` ( A ( -v ` U ) Z ) ) ) |
10 |
|
eqid |
|- ( +v ` U ) = ( +v ` U ) |
11 |
|
eqid |
|- ( .sOLD ` U ) = ( .sOLD ` U ) |
12 |
1 10 11 7
|
nvmval |
|- ( ( U e. NrmCVec /\ A e. X /\ Z e. X ) -> ( A ( -v ` U ) Z ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) |
13 |
6 12
|
mpd3an3 |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( -v ` U ) Z ) = ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) ) |
14 |
|
neg1cn |
|- -u 1 e. CC |
15 |
11 2
|
nvsz |
|- ( ( U e. NrmCVec /\ -u 1 e. CC ) -> ( -u 1 ( .sOLD ` U ) Z ) = Z ) |
16 |
14 15
|
mpan2 |
|- ( U e. NrmCVec -> ( -u 1 ( .sOLD ` U ) Z ) = Z ) |
17 |
16
|
oveq2d |
|- ( U e. NrmCVec -> ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) = ( A ( +v ` U ) Z ) ) |
18 |
17
|
adantr |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) ( -u 1 ( .sOLD ` U ) Z ) ) = ( A ( +v ` U ) Z ) ) |
19 |
1 10 2
|
nv0rid |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( +v ` U ) Z ) = A ) |
20 |
13 18 19
|
3eqtrd |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( A ( -v ` U ) Z ) = A ) |
21 |
20
|
fveq2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` ( A ( -v ` U ) Z ) ) = ( N ` A ) ) |
22 |
9 21
|
eqtr2d |
|- ( ( U e. NrmCVec /\ A e. X ) -> ( N ` A ) = ( A D Z ) ) |