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

Metamath Proof Explorer

Theorem hoadd32i

Description: Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hods.1	$⊢ R : ℋ ⟶ ℋ$
	hods.2	$⊢ S : ℋ ⟶ ℋ$
	hods.3	$⊢ T : ℋ ⟶ ℋ$
Assertion	hoadd32i	$⊢ (R +_{op} S) +_{op} T = (R +_{op} T) +_{op} S$

Proof

Step	Hyp	Ref	Expression
1		hods.1	$⊢ R : ℋ ⟶ ℋ$
2		hods.2	$⊢ S : ℋ ⟶ ℋ$
3		hods.3	$⊢ T : ℋ ⟶ ℋ$
4	2 3	hoaddcomi	$⊢ S +_{op} T = T +_{op} S$
5	4	oveq2i	$⊢ R +_{op} (S +_{op} T) = R +_{op} (T +_{op} S)$
6	1 2 3	hoaddassi	$⊢ (R +_{op} S) +_{op} T = R +_{op} (S +_{op} T)$
7	1 3 2	hoaddassi	$⊢ (R +_{op} T) +_{op} S = R +_{op} (T +_{op} S)$
8	5 6 7	3eqtr4i	$⊢ (R +_{op} S) +_{op} T = (R +_{op} T) +_{op} S$