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 ) )