hosubsub4

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

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

Step	Hyp	Ref	Expression
1		neg1cn	$⊢ - 1 \in ℂ$
2		homulcl	$⊢ (- 1 \in ℂ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
3	1 2	mpan	$⊢ U : ℋ ⟶ ℋ \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
4		hosubsub	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land (-1 \cdot_{op} U) : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} (-1 \cdot_{op} U)) = (S -_{op} T) +_{op} (-1 \cdot_{op} U)$
5	3 4	syl3an3	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} (-1 \cdot_{op} U)) = (S -_{op} T) +_{op} (-1 \cdot_{op} U)$
6		hosubneg	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T -_{op} (-1 \cdot_{op} U) = T +_{op} U$
7	6	3adant1	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T -_{op} (-1 \cdot_{op} U) = T +_{op} U$
8	7	oveq2d	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S -_{op} (T -_{op} (-1 \cdot_{op} U)) = S -_{op} (T +_{op} U)$
9		hosubcl	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S -_{op} T) : ℋ ⟶ ℋ$
10		honegsub	$⊢ ((S -_{op} T) : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S -_{op} T) +_{op} (-1 \cdot_{op} U) = (S -_{op} T) -_{op} U$
11	9 10	stoic3	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S -_{op} T) +_{op} (-1 \cdot_{op} U) = (S -_{op} T) -_{op} U$
12	5 8 11	3eqtr3rd	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S -_{op} T) -_{op} U = S -_{op} (T +_{op} U)$

Metamath Proof Explorer