Theorem ascl1

Description: The scalar 1 embedded into a left module corresponds to the 1 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	ascl1	$$⊢\phi \to A\left(1_F\right)=1_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	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
6	3 5	syl	$$⊢\phi \to F\in \mathrm{Ring}$$
7		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
8		eqid	$$⊢1_F=1_F$$
9	7 8	ringidcl	$$⊢F\in \mathrm{Ring}\to 1_F\in {\mathrm{Base}}_F$$
10	6 9	syl	$$⊢\phi \to 1_F\in {\mathrm{Base}}_F$$
11		eqid	$$⊢{\cdot }_W={\cdot }_W$$
12		eqid	$$⊢1_W=1_W$$
13	1 2 7 11 12	asclval	$$⊢1_F\in {\mathrm{Base}}_F\to A\left(1_F\right)=1_F{\cdot }_W{1}_W$$
14	10 13	syl	$$⊢\phi \to A\left(1_F\right)=1_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	15 2 11 8	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge 1_W\in {\mathrm{Base}}_W\right)\to 1_F{\cdot }_W{1}_W=1_W$$
19	3 17 18	syl2anc	$$⊢\phi \to 1_F{\cdot }_W{1}_W=1_W$$
20	14 19	eqtrd	$$⊢\phi \to A\left(1_F\right)=1_W$$