This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sralmod0

Description: The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014)

Ref Expression
Hypotheses sralmod0.a 
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
sralmod0.z 
|- ( ph -> .0. = ( 0g ` W ) )
sralmod0.s 
|- ( ph -> S C_ ( Base ` W ) )
Assertion sralmod0 
|- ( ph -> .0. = ( 0g ` A ) )

Proof

Step Hyp Ref Expression
1 sralmod0.a 
 |-  ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2 sralmod0.z 
 |-  ( ph -> .0. = ( 0g ` W ) )
3 sralmod0.s 
 |-  ( ph -> S C_ ( Base ` W ) )
4 eqidd 
 |-  ( ph -> ( Base ` W ) = ( Base ` W ) )
5 1 3 srabase 
 |-  ( ph -> ( Base ` W ) = ( Base ` A ) )
6 1 3 sraaddg 
 |-  ( ph -> ( +g ` W ) = ( +g ` A ) )
7 6 oveqdr 
 |-  ( ( ph /\ ( a e. ( Base ` W ) /\ b e. ( Base ` W ) ) ) -> ( a ( +g ` W ) b ) = ( a ( +g ` A ) b ) )
8 4 5 7 grpidpropd 
 |-  ( ph -> ( 0g ` W ) = ( 0g ` A ) )
9 2 8 eqtrd 
 |-  ( ph -> .0. = ( 0g ` A ) )