Step |
Hyp |
Ref |
Expression |
1 |
|
marep01ma.a |
|- A = ( N Mat R ) |
2 |
|
marep01ma.b |
|- B = ( Base ` A ) |
3 |
|
marep01ma.r |
|- R e. CRing |
4 |
|
marep01ma.0 |
|- .0. = ( 0g ` R ) |
5 |
|
marep01ma.1 |
|- .1. = ( 1r ` R ) |
6 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
7 |
1 2
|
matrcl |
|- ( M e. B -> ( N e. Fin /\ R e. _V ) ) |
8 |
7
|
simpld |
|- ( M e. B -> N e. Fin ) |
9 |
3
|
a1i |
|- ( M e. B -> R e. CRing ) |
10 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
11 |
6 5
|
ringidcl |
|- ( R e. Ring -> .1. e. ( Base ` R ) ) |
12 |
3 10 11
|
mp2b |
|- .1. e. ( Base ` R ) |
13 |
6 4
|
ring0cl |
|- ( R e. Ring -> .0. e. ( Base ` R ) ) |
14 |
3 10 13
|
mp2b |
|- .0. e. ( Base ` R ) |
15 |
12 14
|
ifcli |
|- if ( l = I , .1. , .0. ) e. ( Base ` R ) |
16 |
15
|
a1i |
|- ( ( M e. B /\ k e. N /\ l e. N ) -> if ( l = I , .1. , .0. ) e. ( Base ` R ) ) |
17 |
|
simp2 |
|- ( ( M e. B /\ k e. N /\ l e. N ) -> k e. N ) |
18 |
|
simp3 |
|- ( ( M e. B /\ k e. N /\ l e. N ) -> l e. N ) |
19 |
|
id |
|- ( M e. B -> M e. B ) |
20 |
19 2
|
eleqtrdi |
|- ( M e. B -> M e. ( Base ` A ) ) |
21 |
20
|
3ad2ant1 |
|- ( ( M e. B /\ k e. N /\ l e. N ) -> M e. ( Base ` A ) ) |
22 |
1 6
|
matecl |
|- ( ( k e. N /\ l e. N /\ M e. ( Base ` A ) ) -> ( k M l ) e. ( Base ` R ) ) |
23 |
17 18 21 22
|
syl3anc |
|- ( ( M e. B /\ k e. N /\ l e. N ) -> ( k M l ) e. ( Base ` R ) ) |
24 |
16 23
|
ifcld |
|- ( ( M e. B /\ k e. N /\ l e. N ) -> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) e. ( Base ` R ) ) |
25 |
1 6 2 8 9 24
|
matbas2d |
|- ( M e. B -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) e. B ) |