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 |
|
eqid |
|- ( N matRepV R ) = ( N matRepV R ) |
5 |
1 2 4 3
|
marepvval |
|- ( ( M e. B /\ C e. V /\ K e. N ) -> ( ( M ( N matRepV R ) C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) ) |
6 |
5
|
adantl |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( ( M ( N matRepV R ) C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) ) |
7 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
8 |
1 2
|
matrcl |
|- ( M e. B -> ( N e. Fin /\ R e. _V ) ) |
9 |
8
|
simpld |
|- ( M e. B -> N e. Fin ) |
10 |
9
|
3ad2ant1 |
|- ( ( M e. B /\ C e. V /\ K e. N ) -> N e. Fin ) |
11 |
10
|
adantl |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> N e. Fin ) |
12 |
|
simpl |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> R e. Ring ) |
13 |
|
elmapi |
|- ( C e. ( ( Base ` R ) ^m N ) -> C : N --> ( Base ` R ) ) |
14 |
|
ffvelrn |
|- ( ( C : N --> ( Base ` R ) /\ i e. N ) -> ( C ` i ) e. ( Base ` R ) ) |
15 |
14
|
ex |
|- ( C : N --> ( Base ` R ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) ) |
16 |
13 15
|
syl |
|- ( C e. ( ( Base ` R ) ^m N ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) ) |
17 |
16 3
|
eleq2s |
|- ( C e. V -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) ) |
18 |
17
|
3ad2ant2 |
|- ( ( M e. B /\ C e. V /\ K e. N ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) ) |
19 |
18
|
adantl |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( i e. N -> ( C ` i ) e. ( Base ` R ) ) ) |
20 |
19
|
imp |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N ) -> ( C ` i ) e. ( Base ` R ) ) |
21 |
20
|
3adant3 |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> ( C ` i ) e. ( Base ` R ) ) |
22 |
|
simp2 |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> i e. N ) |
23 |
|
simp3 |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> j e. N ) |
24 |
2
|
eleq2i |
|- ( M e. B <-> M e. ( Base ` A ) ) |
25 |
24
|
biimpi |
|- ( M e. B -> M e. ( Base ` A ) ) |
26 |
25
|
3ad2ant1 |
|- ( ( M e. B /\ C e. V /\ K e. N ) -> M e. ( Base ` A ) ) |
27 |
26
|
adantl |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> M e. ( Base ` A ) ) |
28 |
27
|
3ad2ant1 |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> M e. ( Base ` A ) ) |
29 |
1 7
|
matecl |
|- ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) ) |
30 |
22 23 28 29
|
syl3anc |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> ( i M j ) e. ( Base ` R ) ) |
31 |
21 30
|
ifcld |
|- ( ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) /\ i e. N /\ j e. N ) -> if ( j = K , ( C ` i ) , ( i M j ) ) e. ( Base ` R ) ) |
32 |
1 7 2 11 12 31
|
matbas2d |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) e. B ) |
33 |
6 32
|
eqeltrd |
|- ( ( R e. Ring /\ ( M e. B /\ C e. V /\ K e. N ) ) -> ( ( M ( N matRepV R ) C ) ` K ) e. B ) |