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