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

Metamath Proof Explorer

Theorem hoadd12i

Description: Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

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

Proof

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