This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 - op S + op S - op T = R - op T

Proof

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