Metamath Proof Explorer

Theorem scmatghm

Description: There is a group homomorphism from the additive group of a ring to the additive group of the ring of scalar matrices over this ring. (Contributed by AV, 22-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 )
Assertion scmatghm 
|- ( ( N e. Fin /\ R e. Ring ) -> F e. ( R GrpHom S ) )

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 eqid 
 |-  ( Base ` S ) = ( Base ` S )
9 eqid 
 |-  ( +g ` R ) = ( +g ` R )
10 eqid 
 |-  ( +g ` S ) = ( +g ` S )
11 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
12 11 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Grp )
13 eqid 
 |-  ( Base ` A ) = ( Base ` A )
14 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
15 2 13 1 14 6 scmatsgrp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. ( SubGrp ` A ) )
16 7 subggrp 
 |-  ( C e. ( SubGrp ` A ) -> S e. Grp )
17 15 16 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. Grp )
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 2 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
23 6 ovexi 
 |-  C e. _V
24 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
25 7 24 resssca 
 |-  ( C e. _V -> ( Scalar ` A ) = ( Scalar ` S ) )
26 23 25 mp1i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` A ) = ( Scalar ` S ) )
27 22 26 eqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` S ) )
28 27 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( +g ` R ) = ( +g ` ( Scalar ` S ) ) )
29 28 oveqd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y ( +g ` R ) z ) = ( y ( +g ` ( Scalar ` S ) ) z ) )
30 29 oveq1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( y ( +g ` R ) z ) .* .1. ) = ( ( y ( +g ` ( Scalar ` S ) ) z ) .* .1. ) )
31 30 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y ( +g ` R ) z ) .* .1. ) = ( ( y ( +g ` ( Scalar ` S ) ) z ) .* .1. ) )
32 2 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
33 2 6 scmatlss 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. ( LSubSp ` A ) )
34 eqid 
 |-  ( LSubSp ` A ) = ( LSubSp ` A )
35 7 34 lsslmod 
 |-  ( ( A e. LMod /\ C e. ( LSubSp ` A ) ) -> S e. LMod )
36 32 33 35 syl2anc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. LMod )
37 36 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> S e. LMod )
38 27 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` S ) ) )
39 1 38 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> K = ( Base ` ( Scalar ` S ) ) )
40 39 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. K <-> y e. ( Base ` ( Scalar ` S ) ) ) )
41 40 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. K -> y e. ( Base ` ( Scalar ` S ) ) ) )
42 41 adantrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( y e. K /\ z e. K ) -> y e. ( Base ` ( Scalar ` S ) ) ) )
43 42 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> y e. ( Base ` ( Scalar ` S ) ) )
44 39 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( z e. K <-> z e. ( Base ` ( Scalar ` S ) ) ) )
45 44 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( z e. K -> z e. ( Base ` ( Scalar ` S ) ) ) )
46 45 adantld 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( y e. K /\ z e. K ) -> z e. ( Base ` ( Scalar ` S ) ) ) )
47 46 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> z e. ( Base ` ( Scalar ` S ) ) )
48 2 13 1 14 6 scmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. C )
49 3 a1i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. = ( 1r ` A ) )
50 48 49 19 3eltr4d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` S ) )
51 50 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> .1. e. ( Base ` S ) )
52 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
53 7 4 ressvsca 
 |-  ( C e. _V -> .* = ( .s ` S ) )
54 23 53 ax-mp 
 |-  .* = ( .s ` S )
55 eqid 
 |-  ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
56 eqid 
 |-  ( +g ` ( Scalar ` S ) ) = ( +g ` ( Scalar ` S ) )
57 8 10 52 54 55 56 lmodvsdir 
 |-  ( ( S e. LMod /\ ( y e. ( Base ` ( Scalar ` S ) ) /\ z e. ( Base ` ( Scalar ` S ) ) /\ .1. e. ( Base ` S ) ) ) -> ( ( y ( +g ` ( Scalar ` S ) ) z ) .* .1. ) = ( ( y .* .1. ) ( +g ` S ) ( z .* .1. ) ) )
58 37 43 47 51 57 syl13anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y ( +g ` ( Scalar ` S ) ) z ) .* .1. ) = ( ( y .* .1. ) ( +g ` S ) ( z .* .1. ) ) )
59 31 58 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y ( +g ` R ) z ) .* .1. ) = ( ( y .* .1. ) ( +g ` S ) ( z .* .1. ) ) )
60 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
61 60 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> R e. Ring )
62 60 anim1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( R e. Ring /\ ( y e. K /\ z e. K ) ) )
63 3anass 
 |-  ( ( R e. Ring /\ y e. K /\ z e. K ) <-> ( R e. Ring /\ ( y e. K /\ z e. K ) ) )
64 62 63 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( R e. Ring /\ y e. K /\ z e. K ) )
65 1 9 ringacl 
 |-  ( ( R e. Ring /\ y e. K /\ z e. K ) -> ( y ( +g ` R ) z ) e. K )
66 64 65 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( y ( +g ` R ) z ) e. K )
67 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ ( y ( +g ` R ) z ) e. K ) -> ( F ` ( y ( +g ` R ) z ) ) = ( ( y ( +g ` R ) z ) .* .1. ) )
68 61 66 67 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` ( y ( +g ` R ) z ) ) = ( ( y ( +g ` R ) z ) .* .1. ) )
69 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ y e. K ) -> ( F ` y ) = ( y .* .1. ) )
70 69 ad2ant2lr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` y ) = ( y .* .1. ) )
71 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ z e. K ) -> ( F ` z ) = ( z .* .1. ) )
72 71 ad2ant2l 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` z ) = ( z .* .1. ) )
73 70 72 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( F ` y ) ( +g ` S ) ( F ` z ) ) = ( ( y .* .1. ) ( +g ` S ) ( z .* .1. ) ) )
74 59 68 73 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` ( y ( +g ` R ) z ) ) = ( ( F ` y ) ( +g ` S ) ( F ` z ) ) )
75 1 8 9 10 12 17 21 74 isghmd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F e. ( R GrpHom S ) )