Metamath Proof Explorer


Theorem honpncani

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

Ref Expression
Hypotheses honpncan.1 R:
honpncan.2 S:
honpncan.3 T:
Assertion honpncani R-opS+opS-opT=R-opT

Proof

Step Hyp Ref Expression
1 honpncan.1 R:
2 honpncan.2 S:
3 honpncan.3 T:
4 1 2 hosubcli R-opS:
5 4 2 3 hoaddsubassi R-opS+opS-opT=R-opS+opS-opT
6 1 2 honpcani R-opS+opS=R
7 6 oveq1i R-opS+opS-opT=R-opT
8 5 7 eqtr3i R-opS+opS-opT=R-opT