Step |
Hyp |
Ref |
Expression |
1 |
|
marepvfval.a |
|- A = ( N Mat R ) |
2 |
|
marepvfval.b |
|- B = ( Base ` A ) |
3 |
|
marepvfval.q |
|- Q = ( N matRepV R ) |
4 |
|
marepvfval.v |
|- V = ( ( Base ` R ) ^m N ) |
5 |
1 2
|
matrcl |
|- ( M e. B -> ( N e. Fin /\ R e. _V ) ) |
6 |
5
|
simpld |
|- ( M e. B -> N e. Fin ) |
7 |
6
|
adantr |
|- ( ( M e. B /\ C e. V ) -> N e. Fin ) |
8 |
7
|
mptexd |
|- ( ( M e. B /\ C e. V ) -> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) e. _V ) |
9 |
|
fveq1 |
|- ( c = C -> ( c ` i ) = ( C ` i ) ) |
10 |
9
|
adantl |
|- ( ( m = M /\ c = C ) -> ( c ` i ) = ( C ` i ) ) |
11 |
|
oveq |
|- ( m = M -> ( i m j ) = ( i M j ) ) |
12 |
11
|
adantr |
|- ( ( m = M /\ c = C ) -> ( i m j ) = ( i M j ) ) |
13 |
10 12
|
ifeq12d |
|- ( ( m = M /\ c = C ) -> if ( j = k , ( c ` i ) , ( i m j ) ) = if ( j = k , ( C ` i ) , ( i M j ) ) ) |
14 |
13
|
mpoeq3dv |
|- ( ( m = M /\ c = C ) -> ( i e. N , j e. N |-> if ( j = k , ( c ` i ) , ( i m j ) ) ) = ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) |
15 |
14
|
mpteq2dv |
|- ( ( m = M /\ c = C ) -> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( c ` i ) , ( i m j ) ) ) ) = ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) ) |
16 |
1 2 3 4
|
marepvfval |
|- Q = ( m e. B , c e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( c ` i ) , ( i m j ) ) ) ) ) |
17 |
15 16
|
ovmpoga |
|- ( ( M e. B /\ C e. V /\ ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) e. _V ) -> ( M Q C ) = ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) ) |
18 |
8 17
|
mpd3an3 |
|- ( ( M e. B /\ C e. V ) -> ( M Q C ) = ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( C ` i ) , ( i M j ) ) ) ) ) |