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 ⊢ 𝐾 = ( Base ‘ 𝑅 )
scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
scmatghm.s ⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
scmatmhm.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
scmatmhm.t ⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
Assertion scmatmhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑀 MndHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 scmatrhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 scmatrhmval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 scmatrhmval.o ⊢ 1 = ( 1r ‘ 𝐴 )
4 scmatrhmval.t ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
5 scmatrhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ∗ 1 ) )
6 scmatrhmval.c ⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
7 scmatghm.s ⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
8 scmatmhm.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
9 scmatmhm.t ⊢ 𝑇 = ( mulGrp ‘ 𝑆 )
10 8 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
11 10 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ Mnd )
12 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
13 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
14 2 12 1 13 6 scmatsrng ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ ( SubRing ‘ 𝐴 ) )
15 7 subrgring ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → 𝑆 ∈ Ring )
16 9 ringmgp ⊢ ( 𝑆 ∈ Ring → 𝑇 ∈ Mnd )
17 14 15 16 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ Mnd )
18 1 2 3 4 5 6 scmatf ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ 𝐶 )
19 2 6 7 scmatstrbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )
20 19 feq3d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐹 : 𝐾 ⟶ ( Base ‘ 𝑆 ) ↔ 𝐹 : 𝐾 ⟶ 𝐶 ) )
21 18 20 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
22 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
24 2 1 13 3 4 22 23 scmatscmiddistr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ∗ 1 ) ( .r ‘ 𝐴 ) ( 𝑧 ∗ 1 ) ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∗ 1 ) )
25 7 23 ressmulr ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝑆 ) )
26 14 25 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝑆 ) )
27 26 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝑆 ) )
28 27 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ∗ 1 ) ( .r ‘ 𝐴 ) ( 𝑧 ∗ 1 ) ) = ( ( 𝑦 ∗ 1 ) ( .r ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
29 24 28 eqtr3d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∗ 1 ) = ( ( 𝑦 ∗ 1 ) ( .r ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
30 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑅 ∈ Ring )
32 30 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) )
33 3anass ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ↔ ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) )
34 32 33 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) )
35 1 22 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐾 )
36 34 35 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐾 )
37 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐾 ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∗ 1 ) )
38 31 36 37 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∗ 1 ) )
39 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ∗ 1 ) )
40 39 ad2ant2lr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ∗ 1 ) )
41 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ∗ 1 ) )
42 41 ad2ant2l ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ∗ 1 ) )
43 40 42 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑦 ∗ 1 ) ( .r ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
44 29 38 43 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) )
45 44 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐾 ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) )
46 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
47 1 46 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
48 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝐾 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ∗ 1 ) )
49 30 47 48 syl2anc2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ∗ 1 ) )
50 2 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
51 50 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝐴 ) ) )
52 51 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ 𝑅 ) ∗ 1 ) = ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∗ 1 ) )
53 2 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
54 2 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
55 12 3 ringidcl ⊢ ( 𝐴 ∈ Ring → 1 ∈ ( Base ‘ 𝐴 ) )
56 54 55 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝐴 ) )
57 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
58 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝐴 ) ) = ( 1r ‘ ( Scalar ‘ 𝐴 ) )
59 12 57 4 58 lmodvs1 ⊢ ( ( 𝐴 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝐴 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∗ 1 ) = 1 )
60 53 56 59 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ ( Scalar ‘ 𝐴 ) ) ∗ 1 ) = 1 )
61 52 60 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 1r ‘ 𝑅 ) ∗ 1 ) = 1 )
62 49 61 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = 1 )
63 7 3 subrg1 ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → 1 = ( 1r ‘ 𝑆 ) )
64 14 63 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 = ( 1r ‘ 𝑆 ) )
65 62 64 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
66 21 45 65 3jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐹 : 𝐾 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐾 ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) ) )
67 8 1 mgpbas ⊢ 𝐾 = ( Base ‘ 𝑀 )
68 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
69 9 68 mgpbas ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑇 )
70 8 22 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
71 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
72 9 71 mgpplusg ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ 𝑇 )
73 8 46 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
74 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
75 9 74 ringidval ⊢ ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑇 )
76 67 69 70 72 73 75 ismhm ⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝑇 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( 𝐹 : 𝐾 ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑦 ∈ 𝐾 ∀ 𝑧 ∈ 𝐾 ( 𝐹 ‘ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) ) ) )
77 11 17 66 76 syl21anbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑀 MndHom 𝑇 ) )