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. = ( 1r ` A )
scmatrhmval.t 
|- .* = ( .s ` A )
scmatrhmval.f 
|- F = ( x e. K |-> ( x .* .1. ) )
scmatrhmval.c 
|- C = ( N ScMat R )
Assertion scmatfo 
|- ( ( N e. Fin /\ R e. 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. = ( 1r ` A )
4 scmatrhmval.t 
 |-  .* = ( .s ` A )
5 scmatrhmval.f 
 |-  F = ( x e. K |-> ( x .* .1. ) )
6 scmatrhmval.c 
 |-  C = ( N ScMat R )
7 1 2 3 4 5 6 scmatf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F : K --> C )
8 eqid 
 |-  ( Base ` A ) = ( Base ` A )
9 1 2 8 3 4 6 scmatscmid 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. C ) -> E. c e. K y = ( c .* .1. ) )
10 9 3expa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ y e. C ) -> E. c e. K y = ( c .* .1. ) )
11 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ c e. K ) -> ( F ` c ) = ( c .* .1. ) )
12 11 adantll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ c e. K ) -> ( F ` c ) = ( c .* .1. ) )
13 12 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ c e. K ) -> ( c .* .1. ) = ( F ` c ) )
14 13 eqeq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ c e. K ) -> ( y = ( c .* .1. ) <-> y = ( F ` c ) ) )
15 14 biimpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ c e. K ) -> ( y = ( c .* .1. ) -> y = ( F ` c ) ) )
16 15 reximdva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( E. c e. K y = ( c .* .1. ) -> E. c e. K y = ( F ` c ) ) )
17 16 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ y e. C ) -> ( E. c e. K y = ( c .* .1. ) -> E. c e. K y = ( F ` c ) ) )
18 10 17 mpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ y e. C ) -> E. c e. K y = ( F ` c ) )
19 18 ralrimiva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. y e. C E. c e. K y = ( F ` c ) )
20 dffo3 
 |-  ( F : K -onto-> C <-> ( F : K --> C /\ A. y e. C E. c e. K y = ( F ` c ) ) )
21 7 19 20 sylanbrc 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F : K -onto-> C )