Theorem hoaddsub

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

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

Proof

Step	Hyp	Ref	Expression
1		hoaddcom	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) )
2	1	oveq1d	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑆 +op 𝑇 ) −op 𝑈 ) = ( ( 𝑇 +op 𝑆 ) −op 𝑈 ) )
3	2	3adant3	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( 𝑆 +op 𝑇 ) −op 𝑈 ) = ( ( 𝑇 +op 𝑆 ) −op 𝑈 ) )
4		hoaddsubass	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( 𝑇 +op 𝑆 ) −op 𝑈 ) = ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) )
5	4	3com12	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( 𝑇 +op 𝑆 ) −op 𝑈 ) = ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) )
6		hosubcl	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 −op 𝑈 ) : ℋ ⟶ ℋ )
7		hoaddcom	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝑆 −op 𝑈 ) : ℋ ⟶ ℋ ) → ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) )
8	7	ex	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( 𝑆 −op 𝑈 ) : ℋ ⟶ ℋ → ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) ) )
9	6 8	syl5	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) ) )
10	9	expd	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑆 : ℋ ⟶ ℋ → ( 𝑈 : ℋ ⟶ ℋ → ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) ) ) )
11	10	com12	⊢ ( 𝑆 : ℋ ⟶ ℋ → ( 𝑇 : ℋ ⟶ ℋ → ( 𝑈 : ℋ ⟶ ℋ → ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) ) ) )
12	11	3imp	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 +op ( 𝑆 −op 𝑈 ) ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) )
13	3 5 12	3eqtrd	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( 𝑆 +op 𝑇 ) −op 𝑈 ) = ( ( 𝑆 −op 𝑈 ) +op 𝑇 ) )