Metamath Proof Explorer

Theorem nvaddsub

Description: Commutative/associative law for vector addition and subtraction. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 ⊢ X = BaseSet ⁡ U
nvpncan2.2 ⊢ G = + v ⁡ U
nvpncan2.3 ⊢ M = - v ⁡ U
Assertion nvaddsub ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B M C = A M C G B

Proof

Step Hyp Ref Expression
1 nvpncan2.1 ⊢ X = BaseSet ⁡ U
2 nvpncan2.2 ⊢ G = + v ⁡ U
3 nvpncan2.3 ⊢ M = - v ⁡ U
4 2 nvablo ⊢ U ∈ NrmCVec → G ∈ AbelOp
5 1 2 bafval ⊢ X = ran ⁡ G
6 2 3 vsfval ⊢ M = / g ⁡ G
7 5 6 ablomuldiv ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B M C = A M C G B
8 4 7 sylan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G B M C = A M C G B