Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Semiring left modules
slmd0vlid
Metamath Proof Explorer
Description: Left identity law for the zero vector. ( hvaddid2 analog.)
(Contributed by NM , 10-Jan-2014) (Revised by Mario Carneiro , 19-Jun-2014) (Revised by Thierry Arnoux , 1-Apr-2018)
Ref
Expression
Hypotheses
slmd0vlid.v
⊢ 𝑉 = ( Base ‘ 𝑊 )
slmd0vlid.a
⊢ + = ( +g ‘ 𝑊 )
slmd0vlid.z
⊢ 0 = ( 0g ‘ 𝑊 )
Assertion
slmd0vlid
⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 + 𝑋 ) = 𝑋 )
Proof
Step
Hyp
Ref
Expression
1
slmd0vlid.v
⊢ 𝑉 = ( Base ‘ 𝑊 )
2
slmd0vlid.a
⊢ + = ( +g ‘ 𝑊 )
3
slmd0vlid.z
⊢ 0 = ( 0g ‘ 𝑊 )
4
slmdmnd
⊢ ( 𝑊 ∈ SLMod → 𝑊 ∈ Mnd )
5
1 2 3
mndlid
⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑋 ∈ 𝑉 ) → ( 0 + 𝑋 ) = 𝑋 )
6
4 5
sylan
⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 + 𝑋 ) = 𝑋 )