Theorem ascl0

Description: The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019)

	Ref	Expression
Hypotheses	ascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	ascl0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	ascl0.l	$$⊢\phi \to W\in \mathrm{LMod}$$
	ascl0.r	$$⊢\phi \to W\in \mathrm{Ring}$$
Assertion	ascl0	$$⊢\phi \to A\left(0_F\right)=0_W$$

Proof

Step	Hyp	Ref	Expression
1		ascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		ascl0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		ascl0.l	$$⊢\phi \to W\in \mathrm{LMod}$$
4		ascl0.r	$$⊢\phi \to W\in \mathrm{Ring}$$
5	2	lmodfgrp	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Grp}$$
6		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
7		eqid	$$⊢0_F=0_F$$
8	6 7	grpidcl	$$⊢F\in \mathrm{Grp}\to 0_F\in {\mathrm{Base}}_F$$
9		eqid	$$⊢{\cdot }_W={\cdot }_W$$
10		eqid	$$⊢1_W=1_W$$
11	1 2 6 9 10	asclval	$$⊢0_F\in {\mathrm{Base}}_F\to A\left(0_F\right)=0_F{\cdot }_W{1}_W$$
12	3 5 8 11	4syl	$$⊢\phi \to A\left(0_F\right)=0_F{\cdot }_W{1}_W$$
13		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
14	13 10	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in {\mathrm{Base}}_W$$
15	4 14	syl	$$⊢\phi \to 1_W\in {\mathrm{Base}}_W$$
16		eqid	$$⊢0_W=0_W$$
17	13 2 9 7 16	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge 1_W\in {\mathrm{Base}}_W\right)\to 0_F{\cdot }_W{1}_W=0_W$$
18	3 15 17	syl2anc	$$⊢\phi \to 0_F{\cdot }_W{1}_W=0_W$$
19	12 18	eqtrd	$$⊢\phi \to A\left(0_F\right)=0_W$$