Metamath Proof Explorer


Theorem hopncani

Description: Hilbert space operator cancellation law. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hosd1.2 T:
hosd1.3 U:
Assertion hopncani T+opU-opU=T

Proof

Step Hyp Ref Expression
1 hosd1.2 T:
2 hosd1.3 U:
3 1 2 2 hoaddsubassi T+opU-opU=T+opU-opU
4 2 hodidi U-opU=0hop
5 4 oveq2i T+opU-opU=T+op0hop
6 1 hoaddid1i T+op0hop=T
7 3 5 6 3eqtri T+opU-opU=T