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→ 𝐶 )