# 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 ) ) )`
` |-  ( ( 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 ) ) ) ) )`