Database
BASIC ALGEBRAIC STRUCTURES
Left modules
Definition and basic properties
lmodvpncan
Metamath Proof Explorer
Description: Addition/subtraction cancellation law for vectors. ( hvpncan analog.)
(Contributed by NM , 16-Apr-2014) (Revised by Mario Carneiro , 19-Jun-2014)
Ref
Expression
Hypotheses
lmod4.v
⊢ 𝑉 = ( Base ‘ 𝑊 )
lmod4.p
⊢ + = ( +g ‘ 𝑊 )
lmodvaddsub4.m
⊢ − = ( -g ‘ 𝑊 )
Assertion
lmodvpncan
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
Proof
Step
Hyp
Ref
Expression
1
lmod4.v
⊢ 𝑉 = ( Base ‘ 𝑊 )
2
lmod4.p
⊢ + = ( +g ‘ 𝑊 )
3
lmodvaddsub4.m
⊢ − = ( -g ‘ 𝑊 )
4
lmodgrp
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
5
1 2 3
grppncan
⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )
6
4 5
syl3an1
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 + 𝐵 ) − 𝐵 ) = 𝐴 )