assalactf1o

Description: In an associative algebra A , left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm . (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$
	assalactf1o.1	$⊢ E = RLReg (A)$
	assalactf1o.k	$⊢ K = Scalar (A)$
	assalactf1o.2	$⊢ φ \to K \in DivRing$
	assalactf1o.3	$⊢ φ \to \dim (A) \in ℕ_{0}$
	assalactf1o.c	$⊢ φ \to C \in E$
Assertion	assalactf1o	$⊢ φ \to F : B \underset{1-1 onto}{⟶} B$

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		assalactf1o.1	$⊢ E = RLReg (A)$
6		assalactf1o.k	$⊢ K = Scalar (A)$
7		assalactf1o.2	$⊢ φ \to K \in DivRing$
8		assalactf1o.3	$⊢ φ \to \dim (A) \in ℕ_{0}$
9		assalactf1o.c	$⊢ φ \to C \in E$
10		assalmod	$⊢ A \in AssAlg \to A \in LMod$
11	4 10	syl	$⊢ φ \to A \in LMod$
12	6	islvec	$⊢ A \in LVec \leftrightarrow (A \in LMod \land K \in DivRing)$
13	11 7 12	sylanbrc	$⊢ φ \to A \in LVec$
14	5 1	rrgss	$⊢ E \subseteq B$
15	14 9	sselid	$⊢ φ \to C \in B$
16	1 2 3 4 15	lactlmhm	$⊢ φ \to F \in (A LMHom A)$
17		assaring	$⊢ A \in AssAlg \to A \in Ring$
18	4 17	syl	$⊢ φ \to A \in Ring$
19	18	adantr	$⊢ (φ \land x \in B) \to A \in Ring$
20	15	adantr	$⊢ (φ \land x \in B) \to C \in B$
21		simpr	$⊢ (φ \land x \in B) \to x \in B$
22	1 2 19 20 21	ringcld	$⊢ (φ \land x \in B) \to C \underset{˙}{\cdot} x \in B$
23	22	ralrimiva	$⊢ φ \to \forall x \in B C \underset{˙}{\cdot} x \in B$
24	18	ringgrpd	$⊢ φ \to A \in Grp$
25	24	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to A \in Grp$
26	21	ad2antrr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to x \in B$
27		simplr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to y \in B$
28	9	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \in E$
29		eqid	$⊢ -_{A} = -_{A}$
30	1 29 25 26 27	grpsubcld	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to x -_{A} y \in B$
31	18	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to A \in Ring$
32	15	ad3antrrr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \in B$
33	1 2 29 31 32 26 27	ringsubdi	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \underset{˙}{\cdot} (x -_{A} y) = (C \underset{˙}{\cdot} x) -_{A} (C \underset{˙}{\cdot} y)$
34	22	ad2antrr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \underset{˙}{\cdot} x \in B$
35	1 2 31 32 27	ringcld	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \underset{˙}{\cdot} y \in B$
36		simpr	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y$
37		eqid	$⊢ 0_{A} = 0_{A}$
38	1 37 29	grpsubeq0	$⊢ (A \in Grp \land C \underset{˙}{\cdot} x \in B \land C \underset{˙}{\cdot} y \in B) \to ((C \underset{˙}{\cdot} x) -_{A} (C \underset{˙}{\cdot} y) = 0_{A} \leftrightarrow C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y)$
39	38	biimpar	$⊢ ((A \in Grp \land C \underset{˙}{\cdot} x \in B \land C \underset{˙}{\cdot} y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to (C \underset{˙}{\cdot} x) -_{A} (C \underset{˙}{\cdot} y) = 0_{A}$
40	25 34 35 36 39	syl31anc	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to (C \underset{˙}{\cdot} x) -_{A} (C \underset{˙}{\cdot} y) = 0_{A}$
41	33 40	eqtrd	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to C \underset{˙}{\cdot} (x -_{A} y) = 0_{A}$
42	5 1 2 37	rrgeq0i	$⊢ (C \in E \land x -_{A} y \in B) \to (C \underset{˙}{\cdot} (x -_{A} y) = 0_{A} \to x -_{A} y = 0_{A})$
43	42	imp	$⊢ ((C \in E \land x -_{A} y \in B) \land C \underset{˙}{\cdot} (x -_{A} y) = 0_{A}) \to x -_{A} y = 0_{A}$
44	28 30 41 43	syl21anc	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to x -_{A} y = 0_{A}$
45	1 37 29	grpsubeq0	$⊢ (A \in Grp \land x \in B \land y \in B) \to (x -_{A} y = 0_{A} \leftrightarrow x = y)$
46	45	biimpa	$⊢ ((A \in Grp \land x \in B \land y \in B) \land x -_{A} y = 0_{A}) \to x = y$
47	25 26 27 44 46	syl31anc	$⊢ (((φ \land x \in B) \land y \in B) \land C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y) \to x = y$
48	47	ex	$⊢ ((φ \land x \in B) \land y \in B) \to (C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y \to x = y)$
49	48	anasss	$⊢ (φ \land (x \in B \land y \in B)) \to (C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y \to x = y)$
50	49	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B (C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y \to x = y)$
51		oveq2	$⊢ x = y \to C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y$
52	3 51	f1mpt	$⊢ F : B \underset{1-1}{⟶} B \leftrightarrow (\forall x \in B C \underset{˙}{\cdot} x \in B \land \forall x \in B \forall y \in B (C \underset{˙}{\cdot} x = C \underset{˙}{\cdot} y \to x = y))$
53	23 50 52	sylanbrc	$⊢ φ \to F : B \underset{1-1}{⟶} B$
54	1 13 8 16 53	lvecendof1f1o	$⊢ φ \to F : B \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem assalactf1o

Proof