Metamath Proof Explorer

Theorem rlm0

Description: Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion rlm0 
|- ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )

Proof

Step Hyp Ref Expression
1 rlmval 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
2 1 a1i 
 |-  ( T. -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) )
3 eqidd 
 |-  ( T. -> ( 0g ` R ) = ( 0g ` R ) )
4 ssidd 
 |-  ( T. -> ( Base ` R ) C_ ( Base ` R ) )
5 2 3 4 sralmod0 
 |-  ( T. -> ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) ) )
6 5 mptru 
 |-  ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )