Description: Cancellation law for vector subtraction. ( nnncan1 analog.) (Contributed by NM, 7-Mar-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvmf.1 | |- X = ( BaseSet ` U ) |
|
nvmf.3 | |- M = ( -v ` U ) |
||
Assertion | nvnnncan1 | |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvmf.1 | |- X = ( BaseSet ` U ) |
|
2 | nvmf.3 | |- M = ( -v ` U ) |
|
3 | eqid | |- ( +v ` U ) = ( +v ` U ) |
|
4 | 3 | nvablo | |- ( U e. NrmCVec -> ( +v ` U ) e. AbelOp ) |
5 | 1 3 | bafval | |- X = ran ( +v ` U ) |
6 | 3 2 | vsfval | |- M = ( /g ` ( +v ` U ) ) |
7 | 5 6 | ablonnncan1 | |- ( ( ( +v ` U ) e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) ) |
8 | 4 7 | sylan | |- ( ( U e. NrmCVec /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A M B ) M ( A M C ) ) = ( C M B ) ) |