Theorem honpncani

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

	Ref	Expression
Hypotheses	honpncan.1	⊢ 𝑅 : ℋ ⟶ ℋ
	honpncan.2	⊢ 𝑆 : ℋ ⟶ ℋ
	honpncan.3	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	honpncani	⊢ ( ( 𝑅 −op 𝑆 ) +op ( 𝑆 −op 𝑇 ) ) = ( 𝑅 −op 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		honpncan.1	⊢ 𝑅 : ℋ ⟶ ℋ
2		honpncan.2	⊢ 𝑆 : ℋ ⟶ ℋ
3		honpncan.3	⊢ 𝑇 : ℋ ⟶ ℋ
4	1 2	hosubcli	⊢ ( 𝑅 −op 𝑆 ) : ℋ ⟶ ℋ
5	4 2 3	hoaddsubassi	⊢ ( ( ( 𝑅 −op 𝑆 ) +op 𝑆 ) −op 𝑇 ) = ( ( 𝑅 −op 𝑆 ) +op ( 𝑆 −op 𝑇 ) )
6	1 2	honpcani	⊢ ( ( 𝑅 −op 𝑆 ) +op 𝑆 ) = 𝑅
7	6	oveq1i	⊢ ( ( ( 𝑅 −op 𝑆 ) +op 𝑆 ) −op 𝑇 ) = ( 𝑅 −op 𝑇 )
8	5 7	eqtr3i	⊢ ( ( 𝑅 −op 𝑆 ) +op ( 𝑆 −op 𝑇 ) ) = ( 𝑅 −op 𝑇 )