# 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. ) ) )`
` |-  ( ( 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 )`
` |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L ( .r ` R ) ( 1r ` R ) ) = L )`
` |-  ( ( R e. Ring /\ L e. K ) -> ( L ( .r ` R ) .0. ) = .0. )`
` |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L ( .r ` R ) .0. ) = .0. )`
` |-  ( ( 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. ) )`
` |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L ( .r ` R ) if ( i = j , ( 1r ` R ) , .0. ) ) = if ( i = j , L , .0. ) )`
` |-  ( ( 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. ) ) )`
` |-  ( ( N e. Fin /\ R e. Ring /\ L e. K ) -> ( L .x. ( 1r ` A ) ) = ( i e. N , j e. N |-> if ( i = j , L , .0. ) ) )`