Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐴 )
lactlmhm.m ⊢ · = ( .r ‘ 𝐴 )
lactlmhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 · 𝑥 ) )
lactlmhm.a ⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
assalactf1o.1 ⊢ 𝐸 = ( RLReg ‘ 𝐴 )
assalactf1o.k ⊢ 𝐾 = ( Scalar ‘ 𝐴 )
assalactf1o.2 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
assalactf1o.3 ⊢ ( 𝜑 → ( dim ‘ 𝐴 ) ∈ ℕ0 )
assalactf1o.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐸 )
Assertion assalactf1o ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 lactlmhm.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
2 lactlmhm.m ⊢ · = ( .r ‘ 𝐴 )
3 lactlmhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐶 · 𝑥 ) )
4 lactlmhm.a ⊢ ( 𝜑 → 𝐴 ∈ AssAlg )
5 assalactf1o.1 ⊢ 𝐸 = ( RLReg ‘ 𝐴 )
6 assalactf1o.k ⊢ 𝐾 = ( Scalar ‘ 𝐴 )
7 assalactf1o.2 ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
8 assalactf1o.3 ⊢ ( 𝜑 → ( dim ‘ 𝐴 ) ∈ ℕ0 )
9 assalactf1o.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐸 )
10 assalmod ⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ LMod )
11 4 10 syl ⊢ ( 𝜑 → 𝐴 ∈ LMod )
12 6 islvec ⊢ ( 𝐴 ∈ LVec ↔ ( 𝐴 ∈ LMod ∧ 𝐾 ∈ DivRing ) )
13 11 7 12 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ LVec )
14 5 1 rrgss ⊢ 𝐸 ⊆ 𝐵
15 14 9 sselid ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
16 1 2 3 4 15 lactlmhm ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 LMHom 𝐴 ) )
17 assaring ⊢ ( 𝐴 ∈ AssAlg → 𝐴 ∈ Ring )
18 4 17 syl ⊢ ( 𝜑 → 𝐴 ∈ Ring )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ∈ Ring )
20 15 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
22 1 2 19 20 21 ringcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 · 𝑥 ) ∈ 𝐵 )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 𝐶 · 𝑥 ) ∈ 𝐵 )
24 18 ringgrpd ⊢ ( 𝜑 → 𝐴 ∈ Grp )
25 24 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝐴 ∈ Grp )
26 21 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝑥 ∈ 𝐵 )
27 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝑦 ∈ 𝐵 )
28 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝐶 ∈ 𝐸 )
29 eqid ⊢ ( -g ‘ 𝐴 ) = ( -g ‘ 𝐴 )
30 1 29 25 26 27 grpsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 )
31 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝐴 ∈ Ring )
32 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝐶 ∈ 𝐵 )
33 1 2 29 31 32 26 27 ringsubdi ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝐶 · ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝐶 · 𝑥 ) ( -g ‘ 𝐴 ) ( 𝐶 · 𝑦 ) ) )
34 22 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝐶 · 𝑥 ) ∈ 𝐵 )
35 1 2 31 32 27 ringcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝐶 · 𝑦 ) ∈ 𝐵 )
36 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) )
37 eqid ⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
38 1 37 29 grpsubeq0 ⊢ ( ( 𝐴 ∈ Grp ∧ ( 𝐶 · 𝑥 ) ∈ 𝐵 ∧ ( 𝐶 · 𝑦 ) ∈ 𝐵 ) → ( ( ( 𝐶 · 𝑥 ) ( -g ‘ 𝐴 ) ( 𝐶 · 𝑦 ) ) = ( 0g ‘ 𝐴 ) ↔ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) )
39 38 biimpar ⊢ ( ( ( 𝐴 ∈ Grp ∧ ( 𝐶 · 𝑥 ) ∈ 𝐵 ∧ ( 𝐶 · 𝑦 ) ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( ( 𝐶 · 𝑥 ) ( -g ‘ 𝐴 ) ( 𝐶 · 𝑦 ) ) = ( 0g ‘ 𝐴 ) )
40 25 34 35 36 39 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( ( 𝐶 · 𝑥 ) ( -g ‘ 𝐴 ) ( 𝐶 · 𝑦 ) ) = ( 0g ‘ 𝐴 ) )
41 33 40 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝐶 · ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ) = ( 0g ‘ 𝐴 ) )
42 5 1 2 37 rrgeq0i ⊢ ( ( 𝐶 ∈ 𝐸 ∧ ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) → ( ( 𝐶 · ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ) = ( 0g ‘ 𝐴 ) → ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) = ( 0g ‘ 𝐴 ) ) )
43 42 imp ⊢ ( ( ( 𝐶 ∈ 𝐸 ∧ ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) ∧ ( 𝐶 · ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ) = ( 0g ‘ 𝐴 ) ) → ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) = ( 0g ‘ 𝐴 ) )
44 28 30 41 43 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) = ( 0g ‘ 𝐴 ) )
45 1 37 29 grpsubeq0 ⊢ ( ( 𝐴 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) = ( 0g ‘ 𝐴 ) ↔ 𝑥 = 𝑦 ) )
46 45 biimpa ⊢ ( ( ( 𝐴 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) = ( 0g ‘ 𝐴 ) ) → 𝑥 = 𝑦 )
47 25 26 27 44 46 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) ) → 𝑥 = 𝑦 )
48 47 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) → 𝑥 = 𝑦 ) )
49 48 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) → 𝑥 = 𝑦 ) )
50 49 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) → 𝑥 = 𝑦 ) )
51 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) )
52 3 51 f1mpt ⊢ ( 𝐹 : 𝐵 –1-1→ 𝐵 ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝐶 · 𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐶 · 𝑥 ) = ( 𝐶 · 𝑦 ) → 𝑥 = 𝑦 ) ) )
53 23 50 52 sylanbrc ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐵 )
54 1 13 8 16 53 lvecendof1f1o ⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )