Theorem hosubsub2

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

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

Proof

Step	Hyp	Ref	Expression
1		hosubcl	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑇 −op 𝑈 ) : ℋ ⟶ ℋ )
2		honegsub	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ ( 𝑇 −op 𝑈 ) : ℋ ⟶ ℋ ) → ( 𝑆 +op ( - 1 ·op ( 𝑇 −op 𝑈 ) ) ) = ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) )
3	1 2	sylan2	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( 𝑆 +op ( - 1 ·op ( 𝑇 −op 𝑈 ) ) ) = ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) )
4	3	3impb	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 +op ( - 1 ·op ( 𝑇 −op 𝑈 ) ) ) = ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) )
5		honegsubdi2	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( - 1 ·op ( 𝑇 −op 𝑈 ) ) = ( 𝑈 −op 𝑇 ) )
6	5	oveq2d	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 +op ( - 1 ·op ( 𝑇 −op 𝑈 ) ) ) = ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) )
7	6	3adant1	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 +op ( - 1 ·op ( 𝑇 −op 𝑈 ) ) ) = ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) )
8	4 7	eqtr3d	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( 𝑆 −op ( 𝑇 −op 𝑈 ) ) = ( 𝑆 +op ( 𝑈 −op 𝑇 ) ) )