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. ) ) )