Metamath Proof Explorer

Theorem scmatmhm

Description: There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative group of the ring of scalar matrices over this ring. (Contributed by AV, 29-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k 
|- K = ( Base ` R )
scmatrhmval.a 
|- A = ( N Mat R )
scmatrhmval.o 
|- .1. = ( 1r ` A )
scmatrhmval.t 
|- .* = ( .s ` A )
scmatrhmval.f 
|- F = ( x e. K |-> ( x .* .1. ) )
scmatrhmval.c 
|- C = ( N ScMat R )
scmatghm.s 
|- S = ( A |`s C )
scmatmhm.m 
|- M = ( mulGrp ` R )
scmatmhm.t 
|- T = ( mulGrp ` S )
Assertion scmatmhm 
|- ( ( N e. Fin /\ R e. Ring ) -> F e. ( M MndHom T ) )

Proof

Step Hyp Ref Expression
1 scmatrhmval.k 
 |-  K = ( Base ` R )
2 scmatrhmval.a 
 |-  A = ( N Mat R )
3 scmatrhmval.o 
 |-  .1. = ( 1r ` A )
4 scmatrhmval.t 
 |-  .* = ( .s ` A )
5 scmatrhmval.f 
 |-  F = ( x e. K |-> ( x .* .1. ) )
6 scmatrhmval.c 
 |-  C = ( N ScMat R )
7 scmatghm.s 
 |-  S = ( A |`s C )
8 scmatmhm.m 
 |-  M = ( mulGrp ` R )
9 scmatmhm.t 
 |-  T = ( mulGrp ` S )
10 8 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
11 10 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> M e. Mnd )
12 eqid 
 |-  ( Base ` A ) = ( Base ` A )
13 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
14 2 12 1 13 6 scmatsrng 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. ( SubRing ` A ) )
15 7 subrgring 
 |-  ( C e. ( SubRing ` A ) -> S e. Ring )
16 9 ringmgp 
 |-  ( S e. Ring -> T e. Mnd )
17 14 15 16 3syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. Mnd )
18 1 2 3 4 5 6 scmatf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F : K --> C )
19 2 6 7 scmatstrbas 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` S ) = C )
20 19 feq3d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( F : K --> ( Base ` S ) <-> F : K --> C ) )
21 18 20 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F : K --> ( Base ` S ) )
22 eqid 
 |-  ( .r ` R ) = ( .r ` R )
23 eqid 
 |-  ( .r ` A ) = ( .r ` A )
24 2 1 13 3 4 22 23 scmatscmiddistr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y .* .1. ) ( .r ` A ) ( z .* .1. ) ) = ( ( y ( .r ` R ) z ) .* .1. ) )
25 7 23 ressmulr 
 |-  ( C e. ( SubRing ` A ) -> ( .r ` A ) = ( .r ` S ) )
26 14 25 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .r ` A ) = ( .r ` S ) )
27 26 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( .r ` A ) = ( .r ` S ) )
28 27 oveqd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y .* .1. ) ( .r ` A ) ( z .* .1. ) ) = ( ( y .* .1. ) ( .r ` S ) ( z .* .1. ) ) )
29 24 28 eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y ( .r ` R ) z ) .* .1. ) = ( ( y .* .1. ) ( .r ` S ) ( z .* .1. ) ) )
30 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
31 30 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> R e. Ring )
32 30 anim1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( R e. Ring /\ ( y e. K /\ z e. K ) ) )
33 3anass 
 |-  ( ( R e. Ring /\ y e. K /\ z e. K ) <-> ( R e. Ring /\ ( y e. K /\ z e. K ) ) )
34 32 33 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( R e. Ring /\ y e. K /\ z e. K ) )
35 1 22 ringcl 
 |-  ( ( R e. Ring /\ y e. K /\ z e. K ) -> ( y ( .r ` R ) z ) e. K )
36 34 35 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( y ( .r ` R ) z ) e. K )
37 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ ( y ( .r ` R ) z ) e. K ) -> ( F ` ( y ( .r ` R ) z ) ) = ( ( y ( .r ` R ) z ) .* .1. ) )
38 31 36 37 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` ( y ( .r ` R ) z ) ) = ( ( y ( .r ` R ) z ) .* .1. ) )
39 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ y e. K ) -> ( F ` y ) = ( y .* .1. ) )
40 39 ad2ant2lr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` y ) = ( y .* .1. ) )
41 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ z e. K ) -> ( F ` z ) = ( z .* .1. ) )
42 41 ad2ant2l 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` z ) = ( z .* .1. ) )
43 40 42 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( F ` y ) ( .r ` S ) ( F ` z ) ) = ( ( y .* .1. ) ( .r ` S ) ( z .* .1. ) ) )
44 29 38 43 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` ( y ( .r ` R ) z ) ) = ( ( F ` y ) ( .r ` S ) ( F ` z ) ) )
45 44 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. y e. K A. z e. K ( F ` ( y ( .r ` R ) z ) ) = ( ( F ` y ) ( .r ` S ) ( F ` z ) ) )
46 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
47 1 46 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. K )
48 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. K ) -> ( F ` ( 1r ` R ) ) = ( ( 1r ` R ) .* .1. ) )
49 30 47 48 syl2anc2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( F ` ( 1r ` R ) ) = ( ( 1r ` R ) .* .1. ) )
50 2 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
51 50 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` R ) = ( 1r ` ( Scalar ` A ) ) )
52 51 oveq1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` R ) .* .1. ) = ( ( 1r ` ( Scalar ` A ) ) .* .1. ) )
53 2 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
54 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
55 12 3 ringidcl 
 |-  ( A e. Ring -> .1. e. ( Base ` A ) )
56 54 55 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` A ) )
57 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
58 eqid 
 |-  ( 1r ` ( Scalar ` A ) ) = ( 1r ` ( Scalar ` A ) )
59 12 57 4 58 lmodvs1 
 |-  ( ( A e. LMod /\ .1. e. ( Base ` A ) ) -> ( ( 1r ` ( Scalar ` A ) ) .* .1. ) = .1. )
60 53 56 59 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` ( Scalar ` A ) ) .* .1. ) = .1. )
61 52 60 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` R ) .* .1. ) = .1. )
62 49 61 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( F ` ( 1r ` R ) ) = .1. )
63 7 3 subrg1 
 |-  ( C e. ( SubRing ` A ) -> .1. = ( 1r ` S ) )
64 14 63 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. = ( 1r ` S ) )
65 62 64 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
66 21 45 65 3jca 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( F : K --> ( Base ` S ) /\ A. y e. K A. z e. K ( F ` ( y ( .r ` R ) z ) ) = ( ( F ` y ) ( .r ` S ) ( F ` z ) ) /\ ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) )
67 8 1 mgpbas 
 |-  K = ( Base ` M )
68 eqid 
 |-  ( Base ` S ) = ( Base ` S )
69 9 68 mgpbas 
 |-  ( Base ` S ) = ( Base ` T )
70 8 22 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
71 eqid 
 |-  ( .r ` S ) = ( .r ` S )
72 9 71 mgpplusg 
 |-  ( .r ` S ) = ( +g ` T )
73 8 46 ringidval 
 |-  ( 1r ` R ) = ( 0g ` M )
74 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
75 9 74 ringidval 
 |-  ( 1r ` S ) = ( 0g ` T )
76 67 69 70 72 73 75 ismhm 
 |-  ( F e. ( M MndHom T ) <-> ( ( M e. Mnd /\ T e. Mnd ) /\ ( F : K --> ( Base ` S ) /\ A. y e. K A. z e. K ( F ` ( y ( .r ` R ) z ) ) = ( ( F ` y ) ( .r ` S ) ( F ` z ) ) /\ ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) ) )
77 11 17 66 76 syl21anbrc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F e. ( M MndHom T ) )