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	hoaddid1i	⊢ ( 𝑆 +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 𝑇 ) )