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 = ( algSc ` W )
	assaascl0.f	|- F = ( Scalar ` W )
	assaascl0.w	|- ( ph -> W e. AssAlg )
Assertion	assaascl1	|- ( ph -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )

Proof

Step	Hyp	Ref	Expression
1		assaascl0.a	|- A = ( algSc ` W )
2		assaascl0.f	|- F = ( Scalar ` W )
3		assaascl0.w	|- ( ph -> W e. AssAlg )
4		assalmod	|- ( W e. AssAlg -> W e. LMod )
5	3 4	syl	|- ( ph -> W e. LMod )
6		assaring	|- ( W e. AssAlg -> W e. Ring )
7	3 6	syl	|- ( ph -> W e. Ring )
8	1 2 5 7	ascl1	|- ( ph -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )