hosubid1

Description: The zero operator subtracted from a Hilbert space operator. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hosubid1	$⊢ T : ℋ ⟶ ℋ \to T -_{op} 0_{hop} = T$

Step	Hyp	Ref	Expression
1		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
2		ho0sub	$⊢ (T : ℋ ⟶ ℋ \land 0_{hop} : ℋ ⟶ ℋ) \to T -_{op} 0_{hop} = T +_{op} (0_{hop} -_{op} 0_{hop})$
3	1 2	mpan2	$⊢ T : ℋ ⟶ ℋ \to T -_{op} 0_{hop} = T +_{op} (0_{hop} -_{op} 0_{hop})$
4	1	hodidi	$⊢ 0_{hop} -_{op} 0_{hop} = 0_{hop}$
5	4	oveq2i	$⊢ T +_{op} (0_{hop} -_{op} 0_{hop}) = T +_{op} 0_{hop}$
6		hoaddrid	$⊢ T : ℋ ⟶ ℋ \to T +_{op} 0_{hop} = T$
7	5 6	eqtrid	$⊢ T : ℋ ⟶ ℋ \to T +_{op} (0_{hop} -_{op} 0_{hop}) = T$
8	3 7	eqtrd	$⊢ T : ℋ ⟶ ℋ \to T -_{op} 0_{hop} = T$

Metamath Proof Explorer