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

Metamath Proof Explorer

Theorem hvadd32i

Description: Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvass.1 ⊢ A ∈ ℋ
hvass.2 ⊢ B ∈ ℋ
hvass.3 ⊢ C ∈ ℋ
Assertion hvadd32i ⊢ A + ℎ B + ℎ C = A + ℎ C + ℎ B

Proof

Step Hyp Ref Expression
1 hvass.1 ⊢ A ∈ ℋ
2 hvass.2 ⊢ B ∈ ℋ
3 hvass.3 ⊢ C ∈ ℋ
4 hvadd32 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B + ℎ C = A + ℎ C + ℎ B
5 1 2 3 4 mp3an ⊢ A + ℎ B + ℎ C = A + ℎ C + ℎ B