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