Step |
Hyp |
Ref |
Expression |
1 |
|
submabas.a |
|- A = ( N Mat R ) |
2 |
|
submabas.b |
|- B = ( Base ` A ) |
3 |
|
eqid |
|- ( D Mat R ) = ( D Mat R ) |
4 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
5 |
|
eqid |
|- ( Base ` ( D Mat R ) ) = ( Base ` ( D Mat R ) ) |
6 |
1 2
|
matrcl |
|- ( M e. B -> ( N e. Fin /\ R e. _V ) ) |
7 |
6
|
simpld |
|- ( M e. B -> N e. Fin ) |
8 |
|
ssfi |
|- ( ( N e. Fin /\ D C_ N ) -> D e. Fin ) |
9 |
7 8
|
sylan |
|- ( ( M e. B /\ D C_ N ) -> D e. Fin ) |
10 |
6
|
simprd |
|- ( M e. B -> R e. _V ) |
11 |
10
|
adantr |
|- ( ( M e. B /\ D C_ N ) -> R e. _V ) |
12 |
|
ssel |
|- ( D C_ N -> ( i e. D -> i e. N ) ) |
13 |
12
|
adantl |
|- ( ( M e. B /\ D C_ N ) -> ( i e. D -> i e. N ) ) |
14 |
13
|
imp |
|- ( ( ( M e. B /\ D C_ N ) /\ i e. D ) -> i e. N ) |
15 |
14
|
3adant3 |
|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> i e. N ) |
16 |
|
ssel |
|- ( D C_ N -> ( j e. D -> j e. N ) ) |
17 |
16
|
adantl |
|- ( ( M e. B /\ D C_ N ) -> ( j e. D -> j e. N ) ) |
18 |
17
|
imp |
|- ( ( ( M e. B /\ D C_ N ) /\ j e. D ) -> j e. N ) |
19 |
18
|
3adant2 |
|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> j e. N ) |
20 |
2
|
eleq2i |
|- ( M e. B <-> M e. ( Base ` A ) ) |
21 |
20
|
biimpi |
|- ( M e. B -> M e. ( Base ` A ) ) |
22 |
21
|
adantr |
|- ( ( M e. B /\ D C_ N ) -> M e. ( Base ` A ) ) |
23 |
22
|
3ad2ant1 |
|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> M e. ( Base ` A ) ) |
24 |
1 4
|
matecl |
|- ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) ) |
25 |
15 19 23 24
|
syl3anc |
|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> ( i M j ) e. ( Base ` R ) ) |
26 |
3 4 5 9 11 25
|
matbas2d |
|- ( ( M e. B /\ D C_ N ) -> ( i e. D , j e. D |-> ( i M j ) ) e. ( Base ` ( D Mat R ) ) ) |