hosubsub2

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

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

Step	Hyp	Ref	Expression
1		hosubcl	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T -_{op} U) : ℋ ⟶ ℋ$
2		honegsub	$⊢ (S : ℋ ⟶ ℋ \land (T -_{op} U) : ℋ ⟶ ℋ) \to S +_{op} (-1 \cdot_{op} (T -_{op} U)) = S -_{op} (T -_{op} U)$
3	1 2	sylan2	$⊢ (S : ℋ ⟶ ℋ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to S +_{op} (-1 \cdot_{op} (T -_{op} U)) = S -_{op} (T -_{op} U)$
4	3	3impb	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S +_{op} (-1 \cdot_{op} (T -_{op} U)) = S -_{op} (T -_{op} U)$
5		honegsubdi2	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T -_{op} U) = U -_{op} T$
6	5	oveq2d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S +_{op} (-1 \cdot_{op} (T -_{op} U)) = S +_{op} (U -_{op} T)$
7	6	3adant1	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S +_{op} (-1 \cdot_{op} (T -_{op} U)) = S +_{op} (U -_{op} T)$
8	4 7	eqtr3d	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} U) = S +_{op} (U -_{op} T)$

Metamath Proof Explorer