Metamath Proof Explorer

Theorem minmar1fval

Description: First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses minmar1fval.a 
|- A = ( N Mat R )
minmar1fval.b 
|- B = ( Base ` A )
minmar1fval.q 
|- Q = ( N minMatR1 R )
minmar1fval.o 
|- .1. = ( 1r ` R )
minmar1fval.z 
|- .0. = ( 0g ` R )
Assertion minmar1fval 
|- Q = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 minmar1fval.a 
 |-  A = ( N Mat R )
2 minmar1fval.b 
 |-  B = ( Base ` A )
3 minmar1fval.q 
 |-  Q = ( N minMatR1 R )
4 minmar1fval.o 
 |-  .1. = ( 1r ` R )
5 minmar1fval.z 
 |-  .0. = ( 0g ` R )
6 oveq12 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) )
7 6 1 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = A )
8 7 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = ( Base ` A ) )
9 8 2 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = B )
10 simpl 
 |-  ( ( n = N /\ r = R ) -> n = N )
11 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
12 11 4 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
13 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
14 13 5 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
15 12 14 ifeq12d 
 |-  ( r = R -> if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) = if ( j = l , .1. , .0. ) )
16 15 ifeq1d 
 |-  ( r = R -> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) = if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) )
17 16 adantl 
 |-  ( ( n = N /\ r = R ) -> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) = if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) )
18 10 10 17 mpoeq123dv 
 |-  ( ( n = N /\ r = R ) -> ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) ) = ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) )
19 10 10 18 mpoeq123dv 
 |-  ( ( n = N /\ r = R ) -> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) ) ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) )
20 9 19 mpteq12dv 
 |-  ( ( n = N /\ r = R ) -> ( m e. ( Base ` ( n Mat r ) ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) ) ) ) = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) )
21 df-minmar1 
 |-  minMatR1 = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , ( 1r ` r ) , ( 0g ` r ) ) , ( i m j ) ) ) ) ) )
22 2 fvexi 
 |-  B e. _V
23 22 mptex 
 |-  ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) e. _V
24 20 21 23 ovmpoa 
 |-  ( ( N e. _V /\ R e. _V ) -> ( N minMatR1 R ) = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) )
25 21 mpondm0 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N minMatR1 R ) = (/) )
26 mpt0 
 |-  ( m e. (/) |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) = (/)
27 25 26 eqtr4di 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N minMatR1 R ) = ( m e. (/) |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) )
28 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
29 2 28 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
30 matbas0pc 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( Base ` ( N Mat R ) ) = (/) )
31 29 30 syl5eq 
 |-  ( -. ( N e. _V /\ R e. _V ) -> B = (/) )
32 31 mpteq1d 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) = ( m e. (/) |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) )
33 27 32 eqtr4d 
 |-  ( -. ( N e. _V /\ R e. _V ) -> ( N minMatR1 R ) = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) ) )
34 24 33 pm2.61i 
 |-  ( N minMatR1 R ) = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) )
35 3 34 eqtri 
 |-  Q = ( m e. B |-> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) ) )