Metamath Proof Explorer

Theorem scmatrhm

Description: There is a ring homomorphism from a ring to 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 ˙ = 1 A
scmatrhmval.t ⊢ ∗ ˙ = ⋅ A
scmatrhmval.f ⊢ F = x ∈ K ⟼ x ∗ ˙ 1 ˙
scmatrhmval.c ⊢ C = N ScMat R
scmatghm.s ⊢ S = A ↾ 𝑠 C
Assertion scmatrhm ⊢ N ∈ Fin ∧ R ∈ Ring → F ∈ R RingHom S

Proof

Step Hyp Ref Expression
1 scmatrhmval.k ⊢ K = Base R
2 scmatrhmval.a ⊢ A = N Mat R
3 scmatrhmval.o ⊢ 1 ˙ = 1 A
4 scmatrhmval.t ⊢ ∗ ˙ = ⋅ A
5 scmatrhmval.f ⊢ F = x ∈ K ⟼ x ∗ ˙ 1 ˙
6 scmatrhmval.c ⊢ C = N ScMat R
7 scmatghm.s ⊢ S = A ↾ 𝑠 C
8 simpr ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Ring
9 eqid ⊢ Base A = Base A
10 eqid ⊢ 0 R = 0 R
11 2 9 1 10 6 scmatsrng ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ SubRing ⁡ A
12 7 subrgring ⊢ C ∈ SubRing ⁡ A → S ∈ Ring
13 11 12 syl ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ Ring
14 1 2 3 4 5 6 7 scmatghm ⊢ N ∈ Fin ∧ R ∈ Ring → F ∈ R GrpHom S
15 eqid ⊢ mulGrp R = mulGrp R
16 eqid ⊢ mulGrp S = mulGrp S
17 1 2 3 4 5 6 7 15 16 scmatmhm ⊢ N ∈ Fin ∧ R ∈ Ring → F ∈ mulGrp R MndHom mulGrp S
18 14 17 jca ⊢ N ∈ Fin ∧ R ∈ Ring → F ∈ R GrpHom S ∧ F ∈ mulGrp R MndHom mulGrp S
19 15 16 isrhm ⊢ F ∈ R RingHom S ↔ R ∈ Ring ∧ S ∈ Ring ∧ F ∈ R GrpHom S ∧ F ∈ mulGrp R MndHom mulGrp S
20 8 13 18 19 syl21anbrc ⊢ N ∈ Fin ∧ R ∈ Ring → F ∈ R RingHom S