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

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 1 2 3 4 5 6 scmatf ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 ⟶ 𝐶 )
8 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
9 1 2 8 3 4 6 scmatscmid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝑐 ∗ 1 ) )
10 9 3expa ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝑐 ∗ 1 ) )
11 1 2 3 4 5 scmatrhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝑐 ∗ 1 ) )
12 11 adantll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝑐 ∗ 1 ) )
13 12 eqcomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑐 ∗ 1 ) = ( 𝐹 ‘ 𝑐 ) )
14 13 eqeq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑦 = ( 𝑐 ∗ 1 ) ↔ 𝑦 = ( 𝐹 ‘ 𝑐 ) ) )
15 14 biimpd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑦 = ( 𝑐 ∗ 1 ) → 𝑦 = ( 𝐹 ‘ 𝑐 ) ) )
16 15 reximdva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝑐 ∗ 1 ) → ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝐹 ‘ 𝑐 ) ) )
17 16 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐶 ) → ( ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝑐 ∗ 1 ) → ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝐹 ‘ 𝑐 ) ) )
18 10 17 mpd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐶 ) → ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝐹 ‘ 𝑐 ) )
19 18 ralrimiva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑦 ∈ 𝐶 ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝐹 ‘ 𝑐 ) )
20 dffo3 ⊢ ( 𝐹 : 𝐾 –onto→ 𝐶 ↔ ( 𝐹 : 𝐾 ⟶ 𝐶 ∧ ∀ 𝑦 ∈ 𝐶 ∃ 𝑐 ∈ 𝐾 𝑦 = ( 𝐹 ‘ 𝑐 ) ) )
21 7 19 20 sylanbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐹 : 𝐾 –onto→ 𝐶 )