Step |
Hyp |
Ref |
Expression |
1 |
|
nvmeq0.1 |
|- X = ( BaseSet ` U ) |
2 |
|
nvmeq0.3 |
|- M = ( -v ` U ) |
3 |
|
nvmeq0.5 |
|- Z = ( 0vec ` U ) |
4 |
1 2
|
nvmcl |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) e. X ) |
5 |
4
|
3expb |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( A M B ) e. X ) |
6 |
1 3
|
nvzcl |
|- ( U e. NrmCVec -> Z e. X ) |
7 |
6
|
adantr |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> Z e. X ) |
8 |
|
simprr |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> B e. X ) |
9 |
5 7 8
|
3jca |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( A M B ) e. X /\ Z e. X /\ B e. X ) ) |
10 |
|
eqid |
|- ( +v ` U ) = ( +v ` U ) |
11 |
1 10
|
nvrcan |
|- ( ( U e. NrmCVec /\ ( ( A M B ) e. X /\ Z e. X /\ B e. X ) ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> ( A M B ) = Z ) ) |
12 |
9 11
|
syldan |
|- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X ) ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> ( A M B ) = Z ) ) |
13 |
12
|
3impb |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> ( A M B ) = Z ) ) |
14 |
1 10 2
|
nvnpcan |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) ( +v ` U ) B ) = A ) |
15 |
1 10 3
|
nv0lid |
|- ( ( U e. NrmCVec /\ B e. X ) -> ( Z ( +v ` U ) B ) = B ) |
16 |
15
|
3adant2 |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( Z ( +v ` U ) B ) = B ) |
17 |
14 16
|
eqeq12d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( ( A M B ) ( +v ` U ) B ) = ( Z ( +v ` U ) B ) <-> A = B ) ) |
18 |
13 17
|
bitr3d |
|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A M B ) = Z <-> A = B ) ) |