Metamath Proof Explorer

Theorem scmatrhmcl

Description: The value of the ring homomorphism F is a scalar matrix. (Contributed by AV, 22-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 scmatrhmcl 
|- ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( F ` X ) e. 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 scmatrhmval 
 |-  ( ( R e. Ring /\ X e. K ) -> ( F ` X ) = ( X .* .1. ) )
8 7 3adant1 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( F ` X ) = ( X .* .1. ) )
9 3simpa 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( N e. Fin /\ R e. Ring ) )
10 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> X e. K )
11 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
12 11 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> A e. Ring )
13 eqid 
 |-  ( Base ` A ) = ( Base ` A )
14 13 3 ringidcl 
 |-  ( A e. Ring -> .1. e. ( Base ` A ) )
15 12 14 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> .1. e. ( Base ` A ) )
16 1 2 13 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. K /\ .1. e. ( Base ` A ) ) ) -> ( X .* .1. ) e. ( Base ` A ) )
17 9 10 15 16 syl12anc 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( X .* .1. ) e. ( Base ` A ) )
18 oveq1 
 |-  ( c = X -> ( c .* .1. ) = ( X .* .1. ) )
19 18 eqeq2d 
 |-  ( c = X -> ( ( X .* .1. ) = ( c .* .1. ) <-> ( X .* .1. ) = ( X .* .1. ) ) )
20 19 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ X e. K ) /\ c = X ) -> ( ( X .* .1. ) = ( c .* .1. ) <-> ( X .* .1. ) = ( X .* .1. ) ) )
21 eqidd 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( X .* .1. ) = ( X .* .1. ) )
22 10 20 21 rspcedvd 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> E. c e. K ( X .* .1. ) = ( c .* .1. ) )
23 1 2 13 3 4 6 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( X .* .1. ) e. C <-> ( ( X .* .1. ) e. ( Base ` A ) /\ E. c e. K ( X .* .1. ) = ( c .* .1. ) ) ) )
24 23 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( ( X .* .1. ) e. C <-> ( ( X .* .1. ) e. ( Base ` A ) /\ E. c e. K ( X .* .1. ) = ( c .* .1. ) ) ) )
25 17 22 24 mpbir2and 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( X .* .1. ) e. C )
26 8 25 eqeltrd 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. K ) -> ( F ` X ) e. C )