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	3 5	syl	$$⊢\phi \to F\in \mathrm{Grp}$$
7		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
8		eqid	$$⊢0_F=0_F$$
9	7 8	grpidcl	$$⊢F\in \mathrm{Grp}\to 0_F\in {\mathrm{Base}}_F$$
10	6 9	syl	$$⊢\phi \to 0_F\in {\mathrm{Base}}_F$$
11		eqid	$$⊢{\cdot }_W={\cdot }_W$$
12		eqid	$$⊢1_W=1_W$$
13	1 2 7 11 12	asclval	$$⊢0_F\in {\mathrm{Base}}_F\to A\left(0_F\right)=0_F{\cdot }_W{1}_W$$
14	10 13	syl	$$⊢\phi \to A\left(0_F\right)=0_F{\cdot }_W{1}_W$$
15		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
16	15 12	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in {\mathrm{Base}}_W$$
17	4 16	syl	$$⊢\phi \to 1_W\in {\mathrm{Base}}_W$$
18		eqid	$$⊢0_W=0_W$$
19	15 2 11 8 18	lmod0vs	$$⊢\left(W\in \mathrm{LMod}\wedge 1_W\in {\mathrm{Base}}_W\right)\to 0_F{\cdot }_W{1}_W=0_W$$
20	3 17 19	syl2anc	$$⊢\phi \to 0_F{\cdot }_W{1}_W=0_W$$
21	14 20	eqtrd	$$⊢\phi \to A\left(0_F\right)=0_W$$