Theorem ascl1

Description: The scalar 1 embedded into a left module corresponds to the 1 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	ascl1	|- ( ph -> ( A ` ( 1r ` F ) ) = ( 1r ` 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	lmodring	|- ( W e. LMod -> F e. Ring )
6	3 5	syl	|- ( ph -> F e. Ring )
7		eqid	|- ( Base ` F ) = ( Base ` F )
8		eqid	|- ( 1r ` F ) = ( 1r ` F )
9	7 8	ringidcl	|- ( F e. Ring -> ( 1r ` F ) e. ( Base ` F ) )
10	6 9	syl	|- ( ph -> ( 1r ` F ) e. ( Base ` F ) )
11		eqid	|- ( .s ` W ) = ( .s ` W )
12		eqid	|- ( 1r ` W ) = ( 1r ` W )
13	1 2 7 11 12	asclval	|- ( ( 1r ` F ) e. ( Base ` F ) -> ( A ` ( 1r ` F ) ) = ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) )
14	10 13	syl	|- ( ph -> ( A ` ( 1r ` F ) ) = ( ( 1r ` 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	15 2 11 8	lmodvs1	|- ( ( W e. LMod /\ ( 1r ` W ) e. ( Base ` W ) ) -> ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 1r ` W ) )
19	3 17 18	syl2anc	|- ( ph -> ( ( 1r ` F ) ( .s ` W ) ( 1r ` W ) ) = ( 1r ` W ) )
20	14 19	eqtrd	|- ( ph -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )