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=BaseR
scmatrhmval.a A=NMatR
scmatrhmval.o 1˙=1A
scmatrhmval.t ˙=A
scmatrhmval.f F=xKx˙1˙
scmatrhmval.c C=NScMatR
scmatghm.s S=A𝑠C
scmatmhm.m M=mulGrpR
scmatmhm.t T=mulGrpS
Assertion scmatmhm NFinRRingFMMndHomT

Proof

Step Hyp Ref Expression
1 scmatrhmval.k K=BaseR
2 scmatrhmval.a A=NMatR
3 scmatrhmval.o 1˙=1A
4 scmatrhmval.t ˙=A
5 scmatrhmval.f F=xKx˙1˙
6 scmatrhmval.c C=NScMatR
7 scmatghm.s S=A𝑠C
8 scmatmhm.m M=mulGrpR
9 scmatmhm.t T=mulGrpS
10 8 ringmgp RRingMMnd
11 10 adantl NFinRRingMMnd
12 eqid BaseA=BaseA
13 eqid 0R=0R
14 2 12 1 13 6 scmatsrng NFinRRingCSubRingA
15 7 subrgring CSubRingASRing
16 9 ringmgp SRingTMnd
17 14 15 16 3syl NFinRRingTMnd
18 1 2 3 4 5 6 scmatf NFinRRingF:KC
19 2 6 7 scmatstrbas NFinRRingBaseS=C
20 19 feq3d NFinRRingF:KBaseSF:KC
21 18 20 mpbird NFinRRingF:KBaseS
22 eqid R=R
23 eqid A=A
24 2 1 13 3 4 22 23 scmatscmiddistr NFinRRingyKzKy˙1˙Az˙1˙=yRz˙1˙
25 7 23 ressmulr CSubRingAA=S
26 14 25 syl NFinRRingA=S
27 26 adantr NFinRRingyKzKA=S
28 27 oveqd NFinRRingyKzKy˙1˙Az˙1˙=y˙1˙Sz˙1˙
29 24 28 eqtr3d NFinRRingyKzKyRz˙1˙=y˙1˙Sz˙1˙
30 simpr NFinRRingRRing
31 30 adantr NFinRRingyKzKRRing
32 30 anim1i NFinRRingyKzKRRingyKzK
33 3anass RRingyKzKRRingyKzK
34 32 33 sylibr NFinRRingyKzKRRingyKzK
35 1 22 ringcl RRingyKzKyRzK
36 34 35 syl NFinRRingyKzKyRzK
37 1 2 3 4 5 scmatrhmval RRingyRzKFyRz=yRz˙1˙
38 31 36 37 syl2anc NFinRRingyKzKFyRz=yRz˙1˙
39 1 2 3 4 5 scmatrhmval RRingyKFy=y˙1˙
40 39 ad2ant2lr NFinRRingyKzKFy=y˙1˙
41 1 2 3 4 5 scmatrhmval RRingzKFz=z˙1˙
42 41 ad2ant2l NFinRRingyKzKFz=z˙1˙
43 40 42 oveq12d NFinRRingyKzKFySFz=y˙1˙Sz˙1˙
44 29 38 43 3eqtr4d NFinRRingyKzKFyRz=FySFz
45 44 ralrimivva NFinRRingyKzKFyRz=FySFz
46 eqid 1R=1R
47 1 46 ringidcl RRing1RK
48 1 2 3 4 5 scmatrhmval RRing1RKF1R=1R˙1˙
49 30 47 48 syl2anc2 NFinRRingF1R=1R˙1˙
50 2 matsca2 NFinRRingR=ScalarA
51 50 fveq2d NFinRRing1R=1ScalarA
52 51 oveq1d NFinRRing1R˙1˙=1ScalarA˙1˙
53 2 matlmod NFinRRingALMod
54 2 matring NFinRRingARing
55 12 3 ringidcl ARing1˙BaseA
56 54 55 syl NFinRRing1˙BaseA
57 eqid ScalarA=ScalarA
58 eqid 1ScalarA=1ScalarA
59 12 57 4 58 lmodvs1 ALMod1˙BaseA1ScalarA˙1˙=1˙
60 53 56 59 syl2anc NFinRRing1ScalarA˙1˙=1˙
61 52 60 eqtrd NFinRRing1R˙1˙=1˙
62 49 61 eqtrd NFinRRingF1R=1˙
63 7 3 subrg1 CSubRingA1˙=1S
64 14 63 syl NFinRRing1˙=1S
65 62 64 eqtrd NFinRRingF1R=1S
66 21 45 65 3jca NFinRRingF:KBaseSyKzKFyRz=FySFzF1R=1S
67 8 1 mgpbas K=BaseM
68 eqid BaseS=BaseS
69 9 68 mgpbas BaseS=BaseT
70 8 22 mgpplusg R=+M
71 eqid S=S
72 9 71 mgpplusg S=+T
73 8 46 ringidval 1R=0M
74 eqid 1S=1S
75 9 74 ringidval 1S=0T
76 67 69 70 72 73 75 ismhm FMMndHomTMMndTMndF:KBaseSyKzKFyRz=FySFzF1R=1S
77 11 17 66 76 syl21anbrc NFinRRingFMMndHomT