Theorem ascl0

Description: The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019)

	Ref	Expression
Hypotheses	ascl0.a	|- A = ( algSc ` W )
	ascl0.f	|- F = ( Scalar ` W )
	ascl0.l	|- ( ph -> W e. LMod )
	ascl0.r	|- ( ph -> W e. Ring )
Assertion	ascl0	|- ( ph -> ( A ` ( 0g ` F ) ) = ( 0g ` W ) )

Proof

Step	Hyp	Ref	Expression
1		ascl0.a	|- A = ( algSc ` W )
2		ascl0.f	|- F = ( Scalar ` W )
3		ascl0.l	|- ( ph -> W e. LMod )
4		ascl0.r	|- ( ph -> W e. Ring )
5	2	lmodfgrp	|- ( W e. LMod -> F e. Grp )
6	3 5	syl	|- ( ph -> F e. Grp )
7		eqid	|- ( Base ` F ) = ( Base ` F )
8		eqid	|- ( 0g ` F ) = ( 0g ` F )
9	7 8	grpidcl	|- ( F e. Grp -> ( 0g ` F ) e. ( Base ` F ) )
10	6 9	syl	|- ( ph -> ( 0g ` F ) e. ( Base ` F ) )
11		eqid	|- ( .s ` W ) = ( .s ` W )
12		eqid	|- ( 1r ` W ) = ( 1r ` W )
13	1 2 7 11 12	asclval	|- ( ( 0g ` F ) e. ( Base ` F ) -> ( A ` ( 0g ` F ) ) = ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) )
14	10 13	syl	|- ( ph -> ( A ` ( 0g ` F ) ) = ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) )
15		eqid	|- ( Base ` W ) = ( Base ` W )
16	15 12	ringidcl	|- ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
17	4 16	syl	|- ( ph -> ( 1r ` W ) e. ( Base ` W ) )
18		eqid	|- ( 0g ` W ) = ( 0g ` W )
19	15 2 11 8 18	lmod0vs	|- ( ( W e. LMod /\ ( 1r ` W ) e. ( Base ` W ) ) -> ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 0g ` W ) )
20	3 17 19	syl2anc	|- ( ph -> ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 0g ` W ) )
21	14 20	eqtrd	|- ( ph -> ( A ` ( 0g ` F ) ) = ( 0g ` W ) )