Database
BASIC ALGEBRAIC STRUCTURES
Left modules
Definition and basic properties
lmodvsubadd
Metamath Proof Explorer
Description: Relationship between vector subtraction and addition. ( hvsubadd analog.) (Contributed by NM , 31-Mar-2014) (Revised by Mario Carneiro , 19-Jun-2014)
Ref
Expression
Hypotheses
lmod4.v
⊢ 𝑉 = ( Base ‘ 𝑊 )
lmod4.p
⊢ + = ( +g ‘ 𝑊 )
lmodvaddsub4.m
⊢ − = ( -g ‘ 𝑊 )
Assertion
lmodvsubadd
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
lmod4.v
⊢ 𝑉 = ( Base ‘ 𝑊 )
2
lmod4.p
⊢ + = ( +g ‘ 𝑊 )
3
lmodvaddsub4.m
⊢ − = ( -g ‘ 𝑊 )
4
lmodabl
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
5
1 2 3
ablsubadd
⊢ ( ( 𝑊 ∈ Abel ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )
6
4 5
sylan
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )