Metamath Proof Explorer

Theorem nvass

Description: The vector addition (group) operation is associative. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvgcl.1 ⊢ X = BaseSet ⁡ U
nvgcl.2 ⊢ G = + v ⁡ U
Assertion nvass ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G B G C

Proof

Step Hyp Ref Expression
1 nvgcl.1 ⊢ X = BaseSet ⁡ U
2 nvgcl.2 ⊢ G = + v ⁡ U
3 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
4 1 2 bafval ⊢ X = ran ⁡ G
5 4 grpoass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G B G C
6 3 5 sylan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B G C = A G B G C