Metamath Proof Explorer

Theorem lactlmhm

Description: In an associative algebra A , left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm . (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses lactlmhm.b 
|- B = ( Base ` A )
lactlmhm.m 
|- .x. = ( .r ` A )
lactlmhm.f 
|- F = ( x e. B |-> ( C .x. x ) )
lactlmhm.a 
|- ( ph -> A e. AssAlg )
lactlmhm.c 
|- ( ph -> C e. B )
Assertion lactlmhm 
|- ( ph -> F e. ( A LMHom A ) )

Proof

Step Hyp Ref Expression
1 lactlmhm.b 
 |-  B = ( Base ` A )
2 lactlmhm.m 
 |-  .x. = ( .r ` A )
3 lactlmhm.f 
 |-  F = ( x e. B |-> ( C .x. x ) )
4 lactlmhm.a 
 |-  ( ph -> A e. AssAlg )
5 lactlmhm.c 
 |-  ( ph -> C e. B )
6 assalmod 
 |-  ( A e. AssAlg -> A e. LMod )
7 4 6 syl 
 |-  ( ph -> A e. LMod )
8 assaring 
 |-  ( A e. AssAlg -> A e. Ring )
9 4 8 syl 
 |-  ( ph -> A e. Ring )
10 1 2 ringlghm 
 |-  ( ( A e. Ring /\ C e. B ) -> ( x e. B |-> ( C .x. x ) ) e. ( A GrpHom A ) )
11 9 5 10 syl2anc 
 |-  ( ph -> ( x e. B |-> ( C .x. x ) ) e. ( A GrpHom A ) )
12 3 11 eqeltrid 
 |-  ( ph -> F e. ( A GrpHom A ) )
13 eqidd 
 |-  ( ph -> ( Scalar ` A ) = ( Scalar ` A ) )
14 4 ad2antrr 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> A e. AssAlg )
15 simplr 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> a e. ( Base ` ( Scalar ` A ) ) )
16 5 ad2antrr 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> C e. B )
17 simpr 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> b e. B )
18 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
19 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
20 eqid 
 |-  ( .s ` A ) = ( .s ` A )
21 1 18 19 20 2 assaassr 
 |-  ( ( A e. AssAlg /\ ( a e. ( Base ` ( Scalar ` A ) ) /\ C e. B /\ b e. B ) ) -> ( C .x. ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( C .x. b ) ) )
22 14 15 16 17 21 syl13anc 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( C .x. ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( C .x. b ) ) )
23 oveq2 
 |-  ( x = ( a ( .s ` A ) b ) -> ( C .x. x ) = ( C .x. ( a ( .s ` A ) b ) ) )
24 7 ad2antrr 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> A e. LMod )
25 1 18 20 19 24 15 17 lmodvscld 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( a ( .s ` A ) b ) e. B )
26 ovexd 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( C .x. ( a ( .s ` A ) b ) ) e. _V )
27 3 23 25 26 fvmptd3 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( F ` ( a ( .s ` A ) b ) ) = ( C .x. ( a ( .s ` A ) b ) ) )
28 oveq2 
 |-  ( x = b -> ( C .x. x ) = ( C .x. b ) )
29 ovexd 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( C .x. b ) e. _V )
30 3 28 17 29 fvmptd3 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( F ` b ) = ( C .x. b ) )
31 30 oveq2d 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( a ( .s ` A ) ( F ` b ) ) = ( a ( .s ` A ) ( C .x. b ) ) )
32 22 27 31 3eqtr4d 
 |-  ( ( ( ph /\ a e. ( Base ` ( Scalar ` A ) ) ) /\ b e. B ) -> ( F ` ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( F ` b ) ) )
33 32 anasss 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` A ) ) /\ b e. B ) ) -> ( F ` ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( F ` b ) ) )
34 33 ralrimivva 
 |-  ( ph -> A. a e. ( Base ` ( Scalar ` A ) ) A. b e. B ( F ` ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( F ` b ) ) )
35 18 18 19 1 20 20 islmhm 
 |-  ( F e. ( A LMHom A ) <-> ( ( A e. LMod /\ A e. LMod ) /\ ( F e. ( A GrpHom A ) /\ ( Scalar ` A ) = ( Scalar ` A ) /\ A. a e. ( Base ` ( Scalar ` A ) ) A. b e. B ( F ` ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( F ` b ) ) ) ) )
36 35 biimpri 
 |-  ( ( ( A e. LMod /\ A e. LMod ) /\ ( F e. ( A GrpHom A ) /\ ( Scalar ` A ) = ( Scalar ` A ) /\ A. a e. ( Base ` ( Scalar ` A ) ) A. b e. B ( F ` ( a ( .s ` A ) b ) ) = ( a ( .s ` A ) ( F ` b ) ) ) ) -> F e. ( A LMHom A ) )
37 7 7 12 13 34 36 syl23anc 
 |-  ( ph -> F e. ( A LMHom A ) )