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	$⊢ S : ℋ ⟶ ℋ$
		hodseq.3	$⊢ T : ℋ ⟶ ℋ$
	Assertion	ho0subi	$⊢ S -_{op} T = S +_{op} (0_{hop} -_{op} T)$

Proof

Step	Hyp	Ref	Expression
1		hodseq.2	$⊢ S : ℋ ⟶ ℋ$
2		hodseq.3	$⊢ T : ℋ ⟶ ℋ$
3		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
4	3 2	hosubcli	$⊢ (0_{hop} -_{op} T) : ℋ ⟶ ℋ$
5	2 1 4	hoadd12i	$⊢ T +_{op} (S +_{op} (0_{hop} -_{op} T)) = S +_{op} (T +_{op} (0_{hop} -_{op} T))$
6	2 3	hodseqi	$⊢ T +_{op} (0_{hop} -_{op} T) = 0_{hop}$
7	6	oveq2i	$⊢ S +_{op} (T +_{op} (0_{hop} -_{op} T)) = S +_{op} 0_{hop}$
8	1	hoaddridi	$⊢ S +_{op} 0_{hop} = S$
9	5 7 8	3eqtri	$⊢ T +_{op} (S +_{op} (0_{hop} -_{op} T)) = S$
10	1 4	hoaddcli	$⊢ (S +_{op} (0_{hop} -_{op} T)) : ℋ ⟶ ℋ$
11	1 2 10	hodsi	$⊢ S -_{op} T = S +_{op} (0_{hop} -_{op} T) \leftrightarrow T +_{op} (S +_{op} (0_{hop} -_{op} T)) = S$
12	9 11	mpbir	$⊢ S -_{op} T = S +_{op} (0_{hop} -_{op} T)$