This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑇 ) ) )