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

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 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
10 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
11 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
12 11 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Grp )
13 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
14 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15 2 13 1 14 6 scmatsgrp ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ ( SubGrp ‘ 𝐴 ) )
16 7 subggrp ⊢ ( 𝐶 ∈ ( SubGrp ‘ 𝐴 ) → 𝑆 ∈ Grp )
17 15 16 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ Grp )
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 2 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
23 6 ovexi ⊢ 𝐶 ∈ V
24 eqid ⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
25 7 24 resssca ⊢ ( 𝐶 ∈ V → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝑆 ) )
26 23 25 mp1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝑆 ) )
27 22 26 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝑆 ) )
28 27 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑆 ) ) )
29 28 oveqd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑆 ) ) 𝑧 ) )
30 29 oveq1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∗ 1 ) = ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑆 ) ) 𝑧 ) ∗ 1 ) )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∗ 1 ) = ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑆 ) ) 𝑧 ) ∗ 1 ) )
32 2 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
33 2 6 scmatlss ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ ( LSubSp ‘ 𝐴 ) )
34 eqid ⊢ ( LSubSp ‘ 𝐴 ) = ( LSubSp ‘ 𝐴 )
35 7 34 lsslmod ⊢ ( ( 𝐴 ∈ LMod ∧ 𝐶 ∈ ( LSubSp ‘ 𝐴 ) ) → 𝑆 ∈ LMod )
36 32 33 35 syl2anc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ LMod )
37 36 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑆 ∈ LMod )
38 27 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
39 1 38 eqtrid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
40 39 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
41 40 biimpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑦 ∈ 𝐾 → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
42 41 adantrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
43 42 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
44 39 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
45 44 biimpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑧 ∈ 𝐾 → 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
46 45 adantld ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ) )
47 46 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
48 2 13 1 14 6 scmatid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐶 )
49 3 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 = ( 1r ‘ 𝐴 ) )
50 48 49 19 3eltr4d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝑆 ) )
51 50 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 1 ∈ ( Base ‘ 𝑆 ) )
52 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
53 7 4 ressvsca ⊢ ( 𝐶 ∈ V → ∗ = ( ·𝑠 ‘ 𝑆 ) )
54 23 53 ax-mp ⊢ ∗ = ( ·𝑠 ‘ 𝑆 )
55 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
56 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑆 ) ) = ( +g ‘ ( Scalar ‘ 𝑆 ) )
57 8 10 52 54 55 56 lmodvsdir ⊢ ( ( 𝑆 ∈ LMod ∧ ( 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 𝑧 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) ∧ 1 ∈ ( Base ‘ 𝑆 ) ) ) → ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑆 ) ) 𝑧 ) ∗ 1 ) = ( ( 𝑦 ∗ 1 ) ( +g ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
58 37 43 47 51 57 syl13anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑆 ) ) 𝑧 ) ∗ 1 ) = ( ( 𝑦 ∗ 1 ) ( +g ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
59 31 58 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∗ 1 ) = ( ( 𝑦 ∗ 1 ) ( +g ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
60 simpr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
61 60 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑅 ∈ Ring )
62 60 anim1i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) )
63 3anass ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ↔ ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) )
64 62 63 sylibr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) )
65 1 9 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐾 )
66 64 65 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐾 )
67 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐾 ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∗ 1 ) )
68 61 66 67 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∗ 1 ) )
69 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ∗ 1 ) )
70 69 ad2ant2lr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ∗ 1 ) )
71 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ∗ 1 ) )
72 71 ad2ant2l ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ∗ 1 ) )
73 70 72 oveq12d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑦 ∗ 1 ) ( +g ‘ 𝑆 ) ( 𝑧 ∗ 1 ) ) )
74 59 68 73 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑧 ) ) )
75 1 8 9 10 12 17 21 74 isghmd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )