hosubsub

Description: Law for double subtraction of Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hosubsub	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} U) = (S -_{op} T) +_{op} U$

Step	Hyp	Ref	Expression
1		hosubsub2	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} U) = S +_{op} (U -_{op} T)$
2		hoaddsubass	$⊢ (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} U) -_{op} T = S +_{op} (U -_{op} T)$
3		hoaddsub	$⊢ (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} U) -_{op} T = (S -_{op} T) +_{op} U$
4	2 3	eqtr3d	$⊢ (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to S +_{op} (U -_{op} T) = (S -_{op} T) +_{op} U$
5	4	3com23	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S +_{op} (U -_{op} T) = (S -_{op} T) +_{op} U$
6	1 5	eqtrd	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} U) = (S -_{op} T) +_{op} U$

Metamath Proof Explorer