Step |
Hyp |
Ref |
Expression |
1 |
|
marepvcl.a |
|- A = ( N Mat R ) |
2 |
|
marepvcl.b |
|- B = ( Base ` A ) |
3 |
|
marepvcl.v |
|- V = ( ( Base ` R ) ^m N ) |
4 |
|
ma1repvcl.1 |
|- .1. = ( 1r ` A ) |
5 |
|
mulmarep1el.0 |
|- .0. = ( 0g ` R ) |
6 |
|
mulmarep1el.e |
|- E = ( ( .1. ( N matRepV R ) C ) ` K ) |
7 |
|
simp3 |
|- ( ( I e. N /\ J e. N /\ L e. N ) -> L e. N ) |
8 |
|
simp2 |
|- ( ( I e. N /\ J e. N /\ L e. N ) -> J e. N ) |
9 |
7 8
|
jca |
|- ( ( I e. N /\ J e. N /\ L e. N ) -> ( L e. N /\ J e. N ) ) |
10 |
1 2 3 4 5 6
|
ma1repveval |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( L e. N /\ J e. N ) ) -> ( L E J ) = if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) |
11 |
9 10
|
syl3an3 |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( L E J ) = if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) |
12 |
11
|
oveq2d |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) ( L E J ) ) = ( ( I X L ) ( .r ` R ) if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) ) |
13 |
|
ovif2 |
|- ( ( I X L ) ( .r ` R ) if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) ) |
14 |
13
|
a1i |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) if ( J = K , ( C ` L ) , if ( J = L , ( 1r ` R ) , .0. ) ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) ) ) |
15 |
|
ovif2 |
|- ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) = if ( J = L , ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) , ( ( I X L ) ( .r ` R ) .0. ) ) |
16 |
|
simp1 |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> R e. Ring ) |
17 |
|
simp1 |
|- ( ( I e. N /\ J e. N /\ L e. N ) -> I e. N ) |
18 |
17
|
3ad2ant3 |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> I e. N ) |
19 |
7
|
3ad2ant3 |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> L e. N ) |
20 |
2
|
eleq2i |
|- ( X e. B <-> X e. ( Base ` A ) ) |
21 |
20
|
biimpi |
|- ( X e. B -> X e. ( Base ` A ) ) |
22 |
21
|
3ad2ant1 |
|- ( ( X e. B /\ C e. V /\ K e. N ) -> X e. ( Base ` A ) ) |
23 |
22
|
3ad2ant2 |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> X e. ( Base ` A ) ) |
24 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
25 |
1 24
|
matecl |
|- ( ( I e. N /\ L e. N /\ X e. ( Base ` A ) ) -> ( I X L ) e. ( Base ` R ) ) |
26 |
18 19 23 25
|
syl3anc |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( I X L ) e. ( Base ` R ) ) |
27 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
28 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
29 |
24 27 28
|
ringridm |
|- ( ( R e. Ring /\ ( I X L ) e. ( Base ` R ) ) -> ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) = ( I X L ) ) |
30 |
16 26 29
|
syl2anc |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) = ( I X L ) ) |
31 |
24 27 5
|
ringrz |
|- ( ( R e. Ring /\ ( I X L ) e. ( Base ` R ) ) -> ( ( I X L ) ( .r ` R ) .0. ) = .0. ) |
32 |
16 26 31
|
syl2anc |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) .0. ) = .0. ) |
33 |
30 32
|
ifeq12d |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> if ( J = L , ( ( I X L ) ( .r ` R ) ( 1r ` R ) ) , ( ( I X L ) ( .r ` R ) .0. ) ) = if ( J = L , ( I X L ) , .0. ) ) |
34 |
15 33
|
eqtrid |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) = if ( J = L , ( I X L ) , .0. ) ) |
35 |
34
|
ifeq2d |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , ( ( I X L ) ( .r ` R ) if ( J = L , ( 1r ` R ) , .0. ) ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , if ( J = L , ( I X L ) , .0. ) ) ) |
36 |
12 14 35
|
3eqtrd |
|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ L e. N ) ) -> ( ( I X L ) ( .r ` R ) ( L E J ) ) = if ( J = K , ( ( I X L ) ( .r ` R ) ( C ` L ) ) , if ( J = L , ( I X L ) , .0. ) ) ) |