This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hoaddsubass

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

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

Proof

Step	Hyp	Ref	Expression
1		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
2		hosubcl	$⊢ (0_{hop} : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (0_{hop} -_{op} U) : ℋ ⟶ ℋ$
3	1 2	mpan	$⊢ U : ℋ ⟶ ℋ \to (0_{hop} -_{op} U) : ℋ ⟶ ℋ$
4		hoaddass	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land (0_{hop} -_{op} U) : ℋ ⟶ ℋ) \to (S +_{op} T) +_{op} (0_{hop} -_{op} U) = S +_{op} (T +_{op} (0_{hop} -_{op} U))$
5	3 4	syl3an3	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S +_{op} T) +_{op} (0_{hop} -_{op} U) = S +_{op} (T +_{op} (0_{hop} -_{op} U))$
6		hoaddcl	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (S +_{op} T) : ℋ ⟶ ℋ$
7		ho0sub	$⊢ ((S +_{op} T) : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S +_{op} T) -_{op} U = (S +_{op} T) +_{op} (0_{hop} -_{op} U)$
8	6 7	stoic3	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S +_{op} T) -_{op} U = (S +_{op} T) +_{op} (0_{hop} -_{op} U)$
9		ho0sub	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T -_{op} U = T +_{op} (0_{hop} -_{op} U)$
10	9	3adant1	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T -_{op} U = T +_{op} (0_{hop} -_{op} U)$
11	10	oveq2d	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S +_{op} (T -_{op} U) = S +_{op} (T +_{op} (0_{hop} -_{op} U))$
12	5 8 11	3eqtr4d	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (S +_{op} T) -_{op} U = S +_{op} (T -_{op} U)$