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

Metamath Proof Explorer

Theorem hoadd4

Description: Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hoadd32	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (R +_{op} S) +_{op} T = (R +_{op} T) +_{op} S$
2	1	oveq1d	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to ((R +_{op} S) +_{op} T) +_{op} U = ((R +_{op} T) +_{op} S) +_{op} U$
3	2	3expa	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land T : ℋ ⟶ ℋ) \to ((R +_{op} S) +_{op} T) +_{op} U = ((R +_{op} T) +_{op} S) +_{op} U$
4	3	adantrr	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to ((R +_{op} S) +_{op} T) +_{op} U = ((R +_{op} T) +_{op} S) +_{op} U$
5		hoaddcl	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \to (R +_{op} S) : ℋ ⟶ ℋ$
6		hoaddass	$⊢ ((R +_{op} S) : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((R +_{op} S) +_{op} T) +_{op} U = (R +_{op} S) +_{op} (T +_{op} U)$
7	6	3expb	$⊢ ((R +_{op} S) : ℋ ⟶ ℋ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to ((R +_{op} S) +_{op} T) +_{op} U = (R +_{op} S) +_{op} (T +_{op} U)$
8	5 7	sylan	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to ((R +_{op} S) +_{op} T) +_{op} U = (R +_{op} S) +_{op} (T +_{op} U)$
9		hoaddcl	$⊢ (R : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (R +_{op} T) : ℋ ⟶ ℋ$
10		hoaddass	$⊢ ((R +_{op} T) : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((R +_{op} T) +_{op} S) +_{op} U = (R +_{op} T) +_{op} (S +_{op} U)$
11	10	3expb	$⊢ ((R +_{op} T) : ℋ ⟶ ℋ \land (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to ((R +_{op} T) +_{op} S) +_{op} U = (R +_{op} T) +_{op} (S +_{op} U)$
12	9 11	sylan	$⊢ ((R : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \land (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to ((R +_{op} T) +_{op} S) +_{op} U = (R +_{op} T) +_{op} (S +_{op} U)$
13	12	an4s	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to ((R +_{op} T) +_{op} S) +_{op} U = (R +_{op} T) +_{op} (S +_{op} U)$
14	4 8 13	3eqtr3d	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) +_{op} (T +_{op} U) = (R +_{op} T) +_{op} (S +_{op} U)$