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

Metamath Proof Explorer

Theorem ho0subi

Description: Subtraction of Hilbert space operators expressed in terms of difference from zero. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hodseq.2 ⊢ 𝑆 : ℋ ⟶ ℋ
hodseq.3 ⊢ 𝑇 : ℋ ⟶ ℋ
Assertion ho0subi ( 𝑆 −op 𝑇 ) = ( 𝑆 +op ( 0hop −op 𝑇 ) )

Proof

Step Hyp Ref Expression
1 hodseq.2 ⊢ 𝑆 : ℋ ⟶ ℋ
2 hodseq.3 ⊢ 𝑇 : ℋ ⟶ ℋ
3 ho0f ⊢ 0hop : ℋ ⟶ ℋ
4 3 2 hosubcli ⊢ ( 0hop −op 𝑇 ) : ℋ ⟶ ℋ
5 2 1 4 hoadd12i ⊢ ( 𝑇 +op ( 𝑆 +op ( 0hop −op 𝑇 ) ) ) = ( 𝑆 +op ( 𝑇 +op ( 0hop −op 𝑇 ) ) )
6 2 3 hodseqi ⊢ ( 𝑇 +op ( 0hop −op 𝑇 ) ) = 0hop
7 6 oveq2i ⊢ ( 𝑆 +op ( 𝑇 +op ( 0hop −op 𝑇 ) ) ) = ( 𝑆 +op 0hop )
8 1 hoaddridi ⊢ ( 𝑆 +op 0hop ) = 𝑆
9 5 7 8 3eqtri ⊢ ( 𝑇 +op ( 𝑆 +op ( 0hop −op 𝑇 ) ) ) = 𝑆
10 1 4 hoaddcli ⊢ ( 𝑆 +op ( 0hop −op 𝑇 ) ) : ℋ ⟶ ℋ
11 1 2 10 hodsi ⊢ ( ( 𝑆 −op 𝑇 ) = ( 𝑆 +op ( 0hop −op 𝑇 ) ) ↔ ( 𝑇 +op ( 𝑆 +op ( 0hop −op 𝑇 ) ) ) = 𝑆 )
12 9 11 mpbir ⊢ ( 𝑆 −op 𝑇 ) = ( 𝑆 +op ( 0hop −op 𝑇 ) )