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

Metamath Proof Explorer

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