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	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
	lactlmhm.f	$⊢ F = (x \in B ⟼ C \underset{˙}{\cdot} x)$
	lactlmhm.a	$⊢ φ \to A \in AssAlg$
	lactlmhm.c	$⊢ φ \to C \in B$
Assertion	lactlmhm	$⊢ φ \to F \in (A LMHom A)$

Proof

Step	Hyp	Ref	Expression
1		lactlmhm.b	$⊢ B = {Base}_{A}$
2		lactlmhm.m	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
3		lactlmhm.f	$⊢ F = (x \in B ⟼ C \underset{˙}{\cdot} x)$
4		lactlmhm.a	$⊢ φ \to A \in AssAlg$
5		lactlmhm.c	$⊢ φ \to C \in B$
6		assalmod	$⊢ A \in AssAlg \to A \in LMod$
7	4 6	syl	$⊢ φ \to A \in LMod$
8		assaring	$⊢ A \in AssAlg \to A \in Ring$
9	4 8	syl	$⊢ φ \to A \in Ring$
10	1 2	ringlghm	$⊢ (A \in Ring \land C \in B) \to (x \in B ⟼ C \underset{˙}{\cdot} x) \in (A GrpHom A)$
11	9 5 10	syl2anc	$⊢ φ \to (x \in B ⟼ C \underset{˙}{\cdot} x) \in (A GrpHom A)$
12	3 11	eqeltrid	$⊢ φ \to F \in (A GrpHom A)$
13		eqidd	$⊢ φ \to Scalar (A) = Scalar (A)$
14	4	ad2antrr	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to A \in AssAlg$
15		simplr	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to a \in {Base}_{Scalar (A)}$
16	5	ad2antrr	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to C \in B$
17		simpr	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to b \in B$
18		eqid	$⊢ Scalar (A) = Scalar (A)$
19		eqid	$⊢ {Base}_{Scalar (A)} = {Base}_{Scalar (A)}$
20		eqid	$⊢ \cdot_{A} = \cdot_{A}$
21	1 18 19 20 2	assaassr	$⊢ (A \in AssAlg \land (a \in {Base}_{Scalar (A)} \land C \in B \land b \in B)) \to C \underset{˙}{\cdot} (a \cdot_{A} b) = a \cdot_{A} (C \underset{˙}{\cdot} b)$
22	14 15 16 17 21	syl13anc	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to C \underset{˙}{\cdot} (a \cdot_{A} b) = a \cdot_{A} (C \underset{˙}{\cdot} b)$
23		oveq2	$⊢ x = a \cdot_{A} b \to C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} (a \cdot_{A} b)$
24	7	ad2antrr	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to A \in LMod$
25	1 18 20 19 24 15 17	lmodvscld	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to a \cdot_{A} b \in B$
26		ovexd	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to C \underset{˙}{\cdot} (a \cdot_{A} b) \in V$
27	3 23 25 26	fvmptd3	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to F (a \cdot_{A} b) = C \underset{˙}{\cdot} (a \cdot_{A} b)$
28		oveq2	$⊢ x = b \to C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} b$
29		ovexd	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to C \underset{˙}{\cdot} b \in V$
30	3 28 17 29	fvmptd3	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to F (b) = C \underset{˙}{\cdot} b$
31	30	oveq2d	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to a \cdot_{A} F (b) = a \cdot_{A} (C \underset{˙}{\cdot} b)$
32	22 27 31	3eqtr4d	$⊢ ((φ \land a \in {Base}_{Scalar (A)}) \land b \in B) \to F (a \cdot_{A} b) = a \cdot_{A} F (b)$
33	32	anasss	$⊢ (φ \land (a \in {Base}_{Scalar (A)} \land b \in B)) \to F (a \cdot_{A} b) = a \cdot_{A} F (b)$
34	33	ralrimivva	$⊢ φ \to \forall a \in {Base}_{Scalar (A)} \forall b \in B F (a \cdot_{A} b) = a \cdot_{A} F (b)$
35	18 18 19 1 20 20	islmhm	$⊢ F \in (A LMHom A) \leftrightarrow ((A \in LMod \land A \in LMod) \land (F \in (A GrpHom A) \land Scalar (A) = Scalar (A) \land \forall a \in {Base}_{Scalar (A)} \forall b \in B F (a \cdot_{A} b) = a \cdot_{A} F (b)))$
36	35	biimpri	$⊢ ((A \in LMod \land A \in LMod) \land (F \in (A GrpHom A) \land Scalar (A) = Scalar (A) \land \forall a \in {Base}_{Scalar (A)} \forall b \in B F (a \cdot_{A} b) = a \cdot_{A} F (b))) \to F \in (A LMHom A)$
37	7 7 12 13 34 36	syl23anc	$⊢ φ \to F \in (A LMHom A)$

Metamath Proof Explorer

Theorem lactlmhm

Proof