Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Algebra
Semiring left modules
slmd0vrid
Metamath Proof Explorer
Description: Right identity law for the zero vector. ( ax-hvaddid 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
slmd0vrid
⊢ ( ( 𝑊 ∈ 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
mndrid
⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 + 0 ) = 𝑋 )
6
4 5
sylan
⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 + 0 ) = 𝑋 )