This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hvpncan |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hvaddcl | ||
| 2 | hvsubval | ||
| 3 | 1 2 | sylancom | |
| 4 | neg1cn | ||
| 5 | hvmulcl | ||
| 6 | 4 5 | mpan | |
| 7 | 6 | ancli | |
| 8 | ax-hvass | ||
| 9 | 8 | 3expb | |
| 10 | 7 9 | sylan2 | |
| 11 | hvnegid | ||
| 12 | 11 | oveq2d | |
| 13 | ax-hvaddid | ||
| 14 | 12 13 | sylan9eqr | |
| 15 | 3 10 14 | 3eqtrd |