# Metamath Proof Explorer

## Theorem minmar1val0

Description: Second 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 minmar1val0
`|- ( M e. B -> ( Q ` M ) = ( 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 1 2 matrcl
` |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )`
7 6 simpld
` |-  ( M e. B -> N e. Fin )`
8 mpoexga
` |-  ( ( N e. Fin /\ N e. Fin ) -> ( 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 )`
9 7 7 8 syl2anc
` |-  ( 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 )`
10 oveq
` |-  ( m = M -> ( i m j ) = ( i M j ) )`
11 10 ifeq2d
` |-  ( m = M -> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) = if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) )`
12 11 mpoeq3dv
` |-  ( m = M -> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i m j ) ) ) = ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) )`
13 12 mpoeq3dv
` |-  ( m = M -> ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( 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 ) ) ) ) )`
14 1 2 3 4 5 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 ) ) ) ) )`
15 13 14 fvmptg
` |-  ( ( 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 ) -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )`
16 9 15 mpdan
` |-  ( M e. B -> ( Q ` M ) = ( k e. N , l e. N |-> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) ) )`