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 3 4
|
marepvval |
|- ( ( M e. B /\ C e. V /\ K e. N ) -> ( ( M Q C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) ) |
6 |
5
|
adantr |
|- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( ( M Q C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) ) |
7 |
|
simprl |
|- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> I e. N ) |
8 |
|
simplrr |
|- ( ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) /\ i = I ) -> J e. N ) |
9 |
|
fvexd |
|- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( C ` i ) e. _V ) |
10 |
|
ovexd |
|- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( i M j ) e. _V ) |
11 |
9 10
|
ifcld |
|- ( ( ( 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 ) |
12 |
11
|
adantr |
|- ( ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( j = K , ( C ` i ) , ( i M j ) ) e. _V ) |
13 |
|
eqeq1 |
|- ( j = J -> ( j = K <-> J = K ) ) |
14 |
13
|
adantl |
|- ( ( i = I /\ j = J ) -> ( j = K <-> J = K ) ) |
15 |
|
fveq2 |
|- ( i = I -> ( C ` i ) = ( C ` I ) ) |
16 |
15
|
adantr |
|- ( ( i = I /\ j = J ) -> ( C ` i ) = ( C ` I ) ) |
17 |
|
oveq12 |
|- ( ( i = I /\ j = J ) -> ( i M j ) = ( I M J ) ) |
18 |
14 16 17
|
ifbieq12d |
|- ( ( i = I /\ j = J ) -> if ( j = K , ( C ` i ) , ( i M j ) ) = if ( J = K , ( C ` I ) , ( I M J ) ) ) |
19 |
18
|
adantl |
|- ( ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( j = K , ( C ` i ) , ( i M j ) ) = if ( J = K , ( C ` I ) , ( I M J ) ) ) |
20 |
7 8 12 19
|
ovmpodv2 |
|- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( ( ( M Q C ) ` K ) = ( i e. N , j e. N |-> if ( j = K , ( C ` i ) , ( i M j ) ) ) -> ( I ( ( M Q C ) ` K ) J ) = if ( J = K , ( C ` I ) , ( I M J ) ) ) ) |
21 |
6 20
|
mpd |
|- ( ( ( M e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( M Q C ) ` K ) J ) = if ( J = K , ( C ` I ) , ( I M J ) ) ) |