Metamath Proof Explorer


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 ) )