# 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 ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({S}{-}_{\mathrm{op}}{T}\right)={R}{-}_{\mathrm{op}}{T}$

### Proof

Step Hyp Ref Expression
1 honpncan.1 ${⊢}{R}:ℋ⟶ℋ$
2 honpncan.2 ${⊢}{S}:ℋ⟶ℋ$
3 honpncan.3 ${⊢}{T}:ℋ⟶ℋ$
4 1 2 hosubcli ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right):ℋ⟶ℋ$
5 4 2 3 hoaddsubassi ${⊢}\left(\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}{T}=\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({S}{-}_{\mathrm{op}}{T}\right)$
6 1 2 honpcani ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{S}={R}$
7 6 oveq1i ${⊢}\left(\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}{S}\right){-}_{\mathrm{op}}{T}={R}{-}_{\mathrm{op}}{T}$
8 5 7 eqtr3i ${⊢}\left({R}{-}_{\mathrm{op}}{S}\right){+}_{\mathrm{op}}\left({S}{-}_{\mathrm{op}}{T}\right)={R}{-}_{\mathrm{op}}{T}$