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

Metamath Proof Explorer

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