Metamath Proof Explorer

Theorem lmodvaddsub4

Description: Vector addition/subtraction law. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmod4.v 
|- V = ( Base ` W )
lmod4.p 
|- .+ = ( +g ` W )
lmodvaddsub4.m 
|- .- = ( -g ` W )
Assertion lmodvaddsub4 
|- ( ( W e. LMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) = ( C .+ D ) <-> ( A .- C ) = ( D .- B ) ) )

Proof

Step Hyp Ref Expression
1 lmod4.v 
 |-  V = ( Base ` W )
2 lmod4.p 
 |-  .+ = ( +g ` W )
3 lmodvaddsub4.m 
 |-  .- = ( -g ` W )
4 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
5 1 2 3 abladdsub4 
 |-  ( ( W e. Abel /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) = ( C .+ D ) <-> ( A .- C ) = ( D .- B ) ) )
6 4 5 syl3an1 
 |-  ( ( W e. LMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) = ( C .+ D ) <-> ( A .- C ) = ( D .- B ) ) )