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		eqid	|- ( Base ` F ) = ( Base ` F )
7		eqid	|- ( 0g ` F ) = ( 0g ` F )
8	6 7	grpidcl	|- ( F e. Grp -> ( 0g ` F ) e. ( Base ` F ) )
9		eqid	|- ( .s ` W ) = ( .s ` W )
10		eqid	|- ( 1r ` W ) = ( 1r ` W )
11	1 2 6 9 10	asclval	|- ( ( 0g ` F ) e. ( Base ` F ) -> ( A ` ( 0g ` F ) ) = ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) )
12	3 5 8 11	4syl	|- ( ph -> ( A ` ( 0g ` F ) ) = ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) )
13		eqid	|- ( Base ` W ) = ( Base ` W )
14	13 10	ringidcl	|- ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
15	4 14	syl	|- ( ph -> ( 1r ` W ) e. ( Base ` W ) )
16		eqid	|- ( 0g ` W ) = ( 0g ` W )
17	13 2 9 7 16	lmod0vs	|- ( ( W e. LMod /\ ( 1r ` W ) e. ( Base ` W ) ) -> ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 0g ` W ) )
18	3 15 17	syl2anc	|- ( ph -> ( ( 0g ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 0g ` W ) )
19	12 18	eqtrd	|- ( ph -> ( A ` ( 0g ` F ) ) = ( 0g ` W ) )