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