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 ⊢ 𝐵 = ( Base ‘ 𝐴 )
lactlmhm.m ⊢ · = ( .r ‘ 𝐴 )
lactlmhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 · 𝑥 ) )
lactlmhm.a ⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
lactlmhm.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion lactlmhm ( 𝜑 → 𝐹 ∈ ( 𝐴 LMHom 𝐴 ) )

Proof

Step Hyp Ref Expression
1 lactlmhm.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
2 lactlmhm.m ⊢ · = ( .r ‘ 𝐴 )
3 lactlmhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 · 𝑥 ) )
4 lactlmhm.a ⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
5 lactlmhm.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
6 assalmod ⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ LMod )
7 4 6 syl ⊢ ( 𝜑 → 𝐴 ∈ LMod )
8 assaring ⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ Ring )
9 4 8 syl ⊢ ( 𝜑 → 𝐴 ∈ Ring )
10 1 2 ringlghm ⊢ ( ( 𝐴 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 · 𝑥 ) ) ∈ ( 𝐴 GrpHom 𝐴 ) )
11 9 5 10 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 · 𝑥 ) ) ∈ ( 𝐴 GrpHom 𝐴 ) )
12 3 11 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 GrpHom 𝐴 ) )
13 eqidd ⊢ ( 𝜑 → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 ) )
14 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ AssAlg )
15 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
16 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
18 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
19 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
20 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
21 1 18 19 20 2 assaassr ⊢ ( ( 𝐴 ∈ AssAlg ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝐶 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐶 · ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐶 · 𝑏 ) ) )
22 14 15 16 17 21 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐶 · ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐶 · 𝑏 ) ) )
23 oveq2 ⊢ ( 𝑥 = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) → ( 𝐶 · 𝑥 ) = ( 𝐶 · ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) )
24 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐴 ∈ LMod )
25 1 18 20 19 24 15 17 lmodvscld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ∈ 𝐵 )
26 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐶 · ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) ∈ V )
27 3 23 25 26 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝐶 · ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) )
28 oveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑏 ) )
29 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐶 · 𝑏 ) ∈ V )
30 3 28 17 29 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐶 · 𝑏 ) )
31 30 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐶 · 𝑏 ) ) )
32 22 27 31 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ) )
33 32 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ) )
34 33 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ) )
35 18 18 19 1 20 20 islmhm ⊢ ( 𝐹 ∈ ( 𝐴 LMHom 𝐴 ) ↔ ( ( 𝐴 ∈ LMod ∧ 𝐴 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝐴 GrpHom 𝐴 ) ∧ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ) ) ) )
36 35 biimpri ⊢ ( ( ( 𝐴 ∈ LMod ∧ 𝐴 ∈ LMod ) ∧ ( 𝐹 ∈ ( 𝐴 GrpHom 𝐴 ) ∧ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∀ 𝑏 ∈ 𝐵 ( 𝐹 ‘ ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑏 ) ) = ( 𝑎 ( ·𝑠 ‘ 𝐴 ) ( 𝐹 ‘ 𝑏 ) ) ) ) → 𝐹 ∈ ( 𝐴 LMHom 𝐴 ) )
37 7 7 12 13 34 36 syl23anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 LMHom 𝐴 ) )