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

Metamath Proof Explorer

Theorem hoadd32

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

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

Proof

Step	Hyp	Ref	Expression
1		hoaddcom	$⊢ (S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to S +_{op} T = T +_{op} S$
2	1	3adant1	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to S +_{op} T = T +_{op} S$
3	2	oveq2d	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to R +_{op} (S +_{op} T) = R +_{op} (T +_{op} S)$
4		hoaddass	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (R +_{op} S) +_{op} T = R +_{op} (S +_{op} T)$
5		hoaddass	$⊢ (R : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \to (R +_{op} T) +_{op} S = R +_{op} (T +_{op} S)$
6	5	3com23	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (R +_{op} T) +_{op} S = R +_{op} (T +_{op} S)$
7	3 4 6	3eqtr4d	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (R +_{op} S) +_{op} T = (R +_{op} T) +_{op} S$