Metamath Proof Explorer

Theorem hvadd4

Description: Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	hvadd4	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to (A +_{ℎ} B) +_{ℎ} (C +_{ℎ} D) = (A +_{ℎ} C) +_{ℎ} (B +_{ℎ} D)$

Proof

Step	Hyp	Ref	Expression
1		hvadd32	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} B) +_{ℎ} C = (A +_{ℎ} C) +_{ℎ} B$
2	1	oveq1d	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to ((A +_{ℎ} B) +_{ℎ} C) +_{ℎ} D = ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D$
3	2	3expa	$⊢ ((A \in ℋ \land B \in ℋ) \land C \in ℋ) \to ((A +_{ℎ} B) +_{ℎ} C) +_{ℎ} D = ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D$
4	3	adantrr	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to ((A +_{ℎ} B) +_{ℎ} C) +_{ℎ} D = ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D$
5		hvaddcl	$⊢ (A \in ℋ \land B \in ℋ) \to A +_{ℎ} B \in ℋ$
6		ax-hvass	$⊢ (A +_{ℎ} B \in ℋ \land C \in ℋ \land D \in ℋ) \to ((A +_{ℎ} B) +_{ℎ} C) +_{ℎ} D = (A +_{ℎ} B) +_{ℎ} (C +_{ℎ} D)$
7	6	3expb	$⊢ (A +_{ℎ} B \in ℋ \land (C \in ℋ \land D \in ℋ)) \to ((A +_{ℎ} B) +_{ℎ} C) +_{ℎ} D = (A +_{ℎ} B) +_{ℎ} (C +_{ℎ} D)$
8	5 7	sylan	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to ((A +_{ℎ} B) +_{ℎ} C) +_{ℎ} D = (A +_{ℎ} B) +_{ℎ} (C +_{ℎ} D)$
9		hvaddcl	$⊢ (A \in ℋ \land C \in ℋ) \to A +_{ℎ} C \in ℋ$
10		ax-hvass	$⊢ (A +_{ℎ} C \in ℋ \land B \in ℋ \land D \in ℋ) \to ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D = (A +_{ℎ} C) +_{ℎ} (B +_{ℎ} D)$
11	10	3expb	$⊢ (A +_{ℎ} C \in ℋ \land (B \in ℋ \land D \in ℋ)) \to ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D = (A +_{ℎ} C) +_{ℎ} (B +_{ℎ} D)$
12	9 11	sylan	$⊢ ((A \in ℋ \land C \in ℋ) \land (B \in ℋ \land D \in ℋ)) \to ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D = (A +_{ℎ} C) +_{ℎ} (B +_{ℎ} D)$
13	12	an4s	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to ((A +_{ℎ} C) +_{ℎ} B) +_{ℎ} D = (A +_{ℎ} C) +_{ℎ} (B +_{ℎ} D)$
14	4 8 13	3eqtr3d	$⊢ ((A \in ℋ \land B \in ℋ) \land (C \in ℋ \land D \in ℋ)) \to (A +_{ℎ} B) +_{ℎ} (C +_{ℎ} D) = (A +_{ℎ} C) +_{ℎ} (B +_{ℎ} D)$