Metamath Proof Explorer


Theorem matsc

Description: The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses matsc.a
|- A = ( N Mat R )
matsc.k
|- K = ( Base ` R )
matsc.m
|- .x. = ( .s ` A )
matsc.z
|- .0. = ( 0g ` R )
Assertion matsc
|- ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L .x. ( 1r ` A ) ) = ( i e. N , j e. N |-> if ( i = j , L , .0. ) ) )

Proof

Step Hyp Ref Expression
1 matsc.a
 |-  A = ( N Mat R )
2 matsc.k
 |-  K = ( Base ` R )
3 matsc.m
 |-  .x. = ( .s ` A )
4 matsc.z
 |-  .0. = ( 0g ` R )
5 simp3
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> L e. K )
6 3simpa
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( N e. Fin /\ R e. Ring ) )
7 1 matring
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
8 eqid
 |-  ( Base ` A ) = ( Base ` A )
9 eqid
 |-  ( 1r ` A ) = ( 1r ` A )
10 8 9 ringidcl
 |-  ( A e. Ring -> ( 1r ` A ) e. ( Base ` A ) )
11 6 7 10 3syl
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( 1r ` A ) e. ( Base ` A ) )
12 eqid
 |-  ( .r ` R ) = ( .r ` R )
13 eqid
 |-  ( N X. N ) = ( N X. N )
14 1 8 2 3 12 13 matvsca2
 |-  ( ( L e. K /\ ( 1r ` A ) e. ( Base ` A ) ) -> ( L .x. ( 1r ` A ) ) = ( ( ( N X. N ) X. { L } ) oF ( .r ` R ) ( 1r ` A ) ) )
15 5 11 14 syl2anc
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L .x. ( 1r ` A ) ) = ( ( ( N X. N ) X. { L } ) oF ( .r ` R ) ( 1r ` A ) ) )
16 simp1
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> N e. Fin )
17 simp13
 |-  ( ( ( N e. Fin /\ R e. Ring /\ L e. K ) /\ i e. N /\ j e. N ) -> L e. K )
18 fvex
 |-  ( 1r ` R ) e. _V
19 4 fvexi
 |-  .0. e. _V
20 18 19 ifex
 |-  if ( i = j , ( 1r ` R ) , .0. ) e. _V
21 20 a1i
 |-  ( ( ( N e. Fin /\ R e. Ring /\ L e. K ) /\ i e. N /\ j e. N ) -> if ( i = j , ( 1r ` R ) , .0. ) e. _V )
22 fconstmpo
 |-  ( ( N X. N ) X. { L } ) = ( i e. N , j e. N |-> L )
23 22 a1i
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( ( N X. N ) X. { L } ) = ( i e. N , j e. N |-> L ) )
24 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
25 1 24 4 mat1
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , .0. ) ) )
26 25 3adant3
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , .0. ) ) )
27 16 16 17 21 23 26 offval22
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( ( ( N X. N ) X. { L } ) oF ( .r ` R ) ( 1r ` A ) ) = ( i e. N , j e. N |-> ( L ( .r ` R ) if ( i = j , ( 1r ` R ) , .0. ) ) ) )
28 ovif2
 |-  ( L ( .r ` R ) if ( i = j , ( 1r ` R ) , .0. ) ) = if ( i = j , ( L ( .r ` R ) ( 1r ` R ) ) , ( L ( .r ` R ) .0. ) )
29 2 12 24 ringridm
 |-  ( ( R e. Ring /\ L e. K ) -> ( L ( .r ` R ) ( 1r ` R ) ) = L )
30 29 3adant1
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L ( .r ` R ) ( 1r ` R ) ) = L )
31 2 12 4 ringrz
 |-  ( ( R e. Ring /\ L e. K ) -> ( L ( .r ` R ) .0. ) = .0. )
32 31 3adant1
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L ( .r ` R ) .0. ) = .0. )
33 30 32 ifeq12d
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> if ( i = j , ( L ( .r ` R ) ( 1r ` R ) ) , ( L ( .r ` R ) .0. ) ) = if ( i = j , L , .0. ) )
34 28 33 eqtrid
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L ( .r ` R ) if ( i = j , ( 1r ` R ) , .0. ) ) = if ( i = j , L , .0. ) )
35 34 mpoeq3dv
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( i e. N , j e. N |-> ( L ( .r ` R ) if ( i = j , ( 1r ` R ) , .0. ) ) ) = ( i e. N , j e. N |-> if ( i = j , L , .0. ) ) )
36 15 27 35 3eqtrd
 |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L .x. ( 1r ` A ) ) = ( i e. N , j e. N |-> if ( i = j , L , .0. ) ) )