Metamath Proof Explorer

Theorem scmatfo

Description: There is a function from a ring onto any ring of scalar matrices over this ring. (Contributed by AV, 26-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k ⊢K=BaseR
scmatrhmval.a ⊢A=NMatR
scmatrhmval.o ⊢1˙=1A
scmatrhmval.t ⊢∗˙=⋅A
scmatrhmval.f ⊢F=x∈K⟼x∗˙1˙
scmatrhmval.c ⊢C=NScMatR
Assertion scmatfo ⊢N∈Fin∧R∈Ring→F:K⟶ontoC

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=x∈K⟼x∗˙1˙
6 scmatrhmval.c ⊢C=NScMatR
7 1 2 3 4 5 6 scmatf ⊢N∈Fin∧R∈Ring→F:K⟶C
8 eqid ⊢BaseA=BaseA
9 1 2 8 3 4 6 scmatscmid ⊢N∈Fin∧R∈Ring∧y∈C→∃c∈Ky=c∗˙1˙
10 9 3expa ⊢N∈Fin∧R∈Ring∧y∈C→∃c∈Ky=c∗˙1˙
11 1 2 3 4 5 scmatrhmval ⊢R∈Ring∧c∈K→F⁡c=c∗˙1˙
12 11 adantll ⊢N∈Fin∧R∈Ring∧c∈K→F⁡c=c∗˙1˙
13 12 eqcomd ⊢N∈Fin∧R∈Ring∧c∈K→c∗˙1˙=F⁡c
14 13 eqeq2d ⊢N∈Fin∧R∈Ring∧c∈K→y=c∗˙1˙↔y=F⁡c
15 14 biimpd ⊢N∈Fin∧R∈Ring∧c∈K→y=c∗˙1˙→y=F⁡c
16 15 reximdva ⊢N∈Fin∧R∈Ring→∃c∈Ky=c∗˙1˙→∃c∈Ky=F⁡c
17 16 adantr ⊢N∈Fin∧R∈Ring∧y∈C→∃c∈Ky=c∗˙1˙→∃c∈Ky=F⁡c
18 10 17 mpd ⊢N∈Fin∧R∈Ring∧y∈C→∃c∈Ky=F⁡c
19 18 ralrimiva ⊢N∈Fin∧R∈Ring→∀y∈C∃c∈Ky=F⁡c
20 dffo3 ⊢F:K⟶ontoC↔F:K⟶C∧∀y∈C∃c∈Ky=F⁡c
21 7 19 20 sylanbrc ⊢N∈Fin∧R∈Ring→F:K⟶ontoC