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 
|- B = ( Base ` A )
lactlmhm.m 
|- .x. = ( .r ` A )
lactlmhm.f 
|- F = ( x e. B |-> ( C .x. x ) )
lactlmhm.a 
|- ( ph -> A e. AssAlg )
assalactf1o.1 
|- E = ( RLReg ` A )
assalactf1o.k 
|- K = ( Scalar ` A )
assalactf1o.2 
|- ( ph -> K e. DivRing )
assalactf1o.3 
|- ( ph -> ( dim ` A ) e. NN0 )
assalactf1o.c 
|- ( ph -> C e. E )
Assertion assalactf1o 
|- ( ph -> F : B -1-1-onto-> B )

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