Theorem hoaddsubi

Description: Law for sum and difference of Hilbert space operators. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

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