Metamath Proof Explorer


Theorem marepvfval

Description: First substitution for the definition of the function replacing a column of a matrix by a vector. (Contributed by AV, 14-Feb-2019) (Revised by AV, 26-Feb-2019) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses marepvfval.a
|- A = ( N Mat R )
marepvfval.b
|- B = ( Base ` A )
marepvfval.q
|- Q = ( N matRepV R )
marepvfval.v
|- V = ( ( Base ` R ) ^m N )
Assertion marepvfval
|- Q = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) )

Proof

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 2 fvexi
 |-  B e. _V
6 4 ovexi
 |-  V e. _V
7 6 a1i
 |-  ( ( N e. _V /\ R e. _V ) -> V e. _V )
8 mpoexga
 |-  ( ( B e. _V /\ V e. _V ) -> ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) e. _V )
9 5 7 8 sylancr
 |-  ( ( N e. _V /\ R e. _V ) -> ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) e. _V )
10 oveq12
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) )
11 10 1 eqtr4di
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = A )
12 11 fveq2d
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = ( Base ` A ) )
13 12 2 eqtr4di
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = B )
14 fveq2
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
15 14 adantl
 |-  ( ( n = N /\ r = R ) -> ( Base ` r ) = ( Base ` R ) )
16 simpl
 |-  ( ( n = N /\ r = R ) -> n = N )
17 15 16 oveq12d
 |-  ( ( n = N /\ r = R ) -> ( ( Base ` r ) ^m n ) = ( ( Base ` R ) ^m N ) )
18 17 4 eqtr4di
 |-  ( ( n = N /\ r = R ) -> ( ( Base ` r ) ^m n ) = V )
19 eqidd
 |-  ( ( n = N /\ r = R ) -> if ( j = k , ( v ` i ) , ( i m j ) ) = if ( j = k , ( v ` i ) , ( i m j ) ) )
20 16 16 19 mpoeq123dv
 |-  ( ( n = N /\ r = R ) -> ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) = ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) )
21 16 20 mpteq12dv
 |-  ( ( n = N /\ r = R ) -> ( k e. n |-> ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) = ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) )
22 13 18 21 mpoeq123dv
 |-  ( ( n = N /\ r = R ) -> ( m e. ( Base ` ( n Mat r ) ) , v e. ( ( Base ` r ) ^m n ) |-> ( k e. n |-> ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) )
23 df-marepv
 |-  matRepV = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) , v e. ( ( Base ` r ) ^m n ) |-> ( k e. n |-> ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) )
24 22 23 ovmpoga
 |-  ( ( N e. _V /\ R e. _V /\ ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) e. _V ) -> ( N matRepV R ) = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) )
25 9 24 mpd3an3
 |-  ( ( N e. _V /\ R e. _V ) -> ( N matRepV R ) = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) )
26 23 mpondm0
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N matRepV R ) = (/) )
27 1 fveq2i
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
28 2 27 eqtri
 |-  B = ( Base ` ( N Mat R ) )
29 matbas0pc
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) )
30 28 29 eqtrid
 |-  ( -. ( N e. _V /\ R e. _V ) -> B = (/) )
31 30 orcd
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( B = (/) \/ V = (/) ) )
32 0mpo0
 |-  ( ( B = (/) \/ V = (/) ) -> ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) = (/) )
33 31 32 syl
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) = (/) )
34 26 33 eqtr4d
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N matRepV R ) = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) ) )
35 25 34 pm2.61i
 |-  ( N matRepV R ) = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) )
36 3 35 eqtri
 |-  Q = ( m e. B , v e. V |-> ( k e. N |-> ( i e. N , j e. N |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) ) )