Theorem assaascl1

Description: The scalar 1 embedded into an associative algebra corresponds to the 1 of the an associative algebra. (Contributed by AV, 31-Jul-2019)

	Ref	Expression
Hypotheses	assaascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	assaascl0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	assaascl0.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
Assertion	assaascl1	$$⊢\phi \to A\left(1_F\right)=1_W$$

Proof

Step	Hyp	Ref	Expression
1		assaascl0.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		assaascl0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		assaascl0.w	$$⊢\phi \to W\in \mathrm{AssAlg}$$
4		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
5	3 4	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
6		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
7	3 6	syl	$$⊢\phi \to W\in \mathrm{Ring}$$
8	1 2 5 7	ascl1	$$⊢\phi \to A\left(1_F\right)=1_W$$