Metamath Proof Explorer

Theorem scmatf

Description: There is a function from a ring to any ring of scalar matrices over this ring. (Contributed by AV, 25-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
Assertion scmatf ⊢ N ∈ Fin ∧ R ∈ Ring → F : K ⟶ C

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 eqid ⊢ Base A = Base A
8 eqid ⊢ 0 R = 0 R
9 2 7 1 8 6 scmatid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ C
10 3 9 eqeltrid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 ˙ ∈ C
11 10 anim1ci ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ K → x ∈ K ∧ 1 ˙ ∈ C
12 1 2 6 4 smatvscl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ K ∧ 1 ˙ ∈ C → x ∗ ˙ 1 ˙ ∈ C
13 11 12 syldan ⊢ N ∈ Fin ∧ R ∈ Ring ∧ x ∈ K → x ∗ ˙ 1 ˙ ∈ C
14 13 5 fmptd ⊢ N ∈ Fin ∧ R ∈ Ring → F : K ⟶ C