Theorem assaascl0

Description: The scalar 0 embedded into an associative algebra corresponds to the 0 of the 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	assaascl0	|- ( ph -> ( A ` ( 0g ` F ) ) = ( 0g ` 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	ascl0	|- ( ph -> ( A ` ( 0g ` F ) ) = ( 0g ` W ) )