| Step |
Hyp |
Ref |
Expression |
| 1 |
|
matbas2.a |
|- A = ( N Mat R ) |
| 2 |
|
matbas2.k |
|- K = ( Base ` R ) |
| 3 |
|
matbas2i.b |
|- B = ( Base ` A ) |
| 4 |
|
matbas2d.n |
|- ( ph -> N e. Fin ) |
| 5 |
|
matbas2d.r |
|- ( ph -> R e. V ) |
| 6 |
|
matbas2d.c |
|- ( ( ph /\ x e. N /\ y e. N ) -> C e. K ) |
| 7 |
6
|
3expb |
|- ( ( ph /\ ( x e. N /\ y e. N ) ) -> C e. K ) |
| 8 |
7
|
ralrimivva |
|- ( ph -> A. x e. N A. y e. N C e. K ) |
| 9 |
|
eqid |
|- ( x e. N , y e. N |-> C ) = ( x e. N , y e. N |-> C ) |
| 10 |
9
|
fmpo |
|- ( A. x e. N A. y e. N C e. K <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) |
| 11 |
8 10
|
sylib |
|- ( ph -> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) |
| 12 |
1 2
|
matbas2 |
|- ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) ) |
| 13 |
4 5 12
|
syl2anc |
|- ( ph -> ( K ^m ( N X. N ) ) = ( Base ` A ) ) |
| 14 |
3 13
|
eqtr4id |
|- ( ph -> B = ( K ^m ( N X. N ) ) ) |
| 15 |
14
|
eleq2d |
|- ( ph -> ( ( x e. N , y e. N |-> C ) e. B <-> ( x e. N , y e. N |-> C ) e. ( K ^m ( N X. N ) ) ) ) |
| 16 |
2
|
fvexi |
|- K e. _V |
| 17 |
4 4
|
xpexd |
|- ( ph -> ( N X. N ) e. _V ) |
| 18 |
|
elmapg |
|- ( ( K e. _V /\ ( N X. N ) e. _V ) -> ( ( x e. N , y e. N |-> C ) e. ( K ^m ( N X. N ) ) <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) ) |
| 19 |
16 17 18
|
sylancr |
|- ( ph -> ( ( x e. N , y e. N |-> C ) e. ( K ^m ( N X. N ) ) <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) ) |
| 20 |
15 19
|
bitrd |
|- ( ph -> ( ( x e. N , y e. N |-> C ) e. B <-> ( x e. N , y e. N |-> C ) : ( N X. N ) --> K ) ) |
| 21 |
11 20
|
mpbird |
|- ( ph -> ( x e. N , y e. N |-> C ) e. B ) |