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 = 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 scmatfo ⊢ N ∈ Fin ∧ R ∈ Ring → F : K ⟶ onto 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 1 2 3 4 5 6 scmatf ⊢ N ∈ Fin ∧ R ∈ Ring → F : K ⟶ C
8 eqid ⊢ Base A = Base A
9 1 2 8 3 4 6 scmatscmid ⊢ N ∈ Fin ∧ R ∈ Ring ∧ y ∈ C → ∃ c ∈ K y = c ∗ ˙ 1 ˙
10 9 3expa ⊢ N ∈ Fin ∧ R ∈ Ring ∧ y ∈ C → ∃ c ∈ K y = 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 ∈ K y = c ∗ ˙ 1 ˙ → ∃ c ∈ K y = F ⁡ c
17 16 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ y ∈ C → ∃ c ∈ K y = c ∗ ˙ 1 ˙ → ∃ c ∈ K y = F ⁡ c
18 10 17 mpd ⊢ N ∈ Fin ∧ R ∈ Ring ∧ y ∈ C → ∃ c ∈ K y = F ⁡ c
19 18 ralrimiva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ y ∈ C ∃ c ∈ K y = F ⁡ c
20 dffo3 ⊢ F : K ⟶ onto C ↔ F : K ⟶ C ∧ ∀ y ∈ C ∃ c ∈ K y = F ⁡ c
21 7 19 20 sylanbrc ⊢ N ∈ Fin ∧ R ∈ Ring → F : K ⟶ onto C