This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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