Metamath Proof Explorer

Theorem hoaddsub

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

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

Proof

Step	Hyp	Ref	Expression
1		hoaddcom	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to S +_{op} T = T +_{op} S$
2	1	oveq1d	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} T) -_{op} U = (T +_{op} S) -_{op} U$
3	2	3adant3	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S +_{op} T) -_{op} U = (T +_{op} S) -_{op} U$
4		hoaddsubass	$⊢ (T : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T +_{op} S) -_{op} U = T +_{op} (S -_{op} U)$
5	4	3com12	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T +_{op} S) -_{op} U = T +_{op} (S -_{op} U)$
6		hosubcl	$⊢ (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S -_{op} U) : ℋ ⟶ ℋ$
7		hoaddcom	$⊢ (T : ℋ ⟶ ℋ \land (S -_{op} U) : ℋ ⟶ ℋ) \to T +_{op} (S -_{op} U) = (S -_{op} U) +_{op} T$
8	7	ex	$⊢ T : ℋ ⟶ ℋ \to ((S -_{op} U) : ℋ ⟶ ℋ \to T +_{op} (S -_{op} U) = (S -_{op} U) +_{op} T)$
9	6 8	syl5	$⊢ T : ℋ ⟶ ℋ \to ((S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (S -_{op} U) = (S -_{op} U) +_{op} T)$
10	9	expd	$⊢ T : ℋ ⟶ ℋ \to (S : ℋ ⟶ ℋ \to (U : ℋ ⟶ ℋ \to T +_{op} (S -_{op} U) = (S -_{op} U) +_{op} T))$
11	10	com12	$⊢ S : ℋ ⟶ ℋ \to (T : ℋ ⟶ ℋ \to (U : ℋ ⟶ ℋ \to T +_{op} (S -_{op} U) = (S -_{op} U) +_{op} T))$
12	11	3imp	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (S -_{op} U) = (S -_{op} U) +_{op} T$
13	3 5 12	3eqtrd	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S +_{op} T) -_{op} U = (S -_{op} U) +_{op} T$