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 syl5eq 
 |-  ( -. ( 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 ) ) ) ) )