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	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
	sralmod0.z	$$⊢\phi \to \underset{\dot{}}{0}=0_W$$
	sralmod0.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
Assertion	sralmod0	$$⊢\phi \to \underset{\dot{}}{0}=0_A$$

Proof

Step	Hyp	Ref	Expression
1		sralmod0.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
2		sralmod0.z	$$⊢\phi \to \underset{\dot{}}{0}=0_W$$
3		sralmod0.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_W$$
5	1 3	srabase	$$⊢\phi \to {\mathrm{Base}}_W={\mathrm{Base}}_A$$
6	1 3	sraaddg	$$⊢\phi \to {+}_W={+}_A$$
7	6	oveqdr	$$⊢\left(\phi \wedge \left(a\in {\mathrm{Base}}_W\wedge b\in {\mathrm{Base}}_W\right)\right)\to a{+}_{W}b=a{+}_{A}b$$
8	4 5 7	grpidpropd	$$⊢\phi \to 0_W=0_A$$
9	2 8	eqtrd	$$⊢\phi \to \underset{\dot{}}{0}=0_A$$