Theorem hosubsub

Description: Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hosubsub	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑇 ) +op 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		hosubsub2	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) = ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) )
2		hoaddsubass	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑆 +op 𝑈 ) −op 𝑇 ) = ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) )
3		hoaddsub	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑆 +op 𝑈 ) −op 𝑇 ) = ( ( 𝑆 −op 𝑇 ) +op 𝑈 ) )
4	2 3	eqtr3d	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) = ( ( 𝑆 −op 𝑇 ) +op 𝑈 ) )
5	4	3com23	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) = ( ( 𝑆 −op 𝑇 ) +op 𝑈 ) )
6	1 5	eqtrd	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑇 ) +op 𝑈 ) )