# Metamath Proof Explorer

## Theorem minmar1eval

Description: An entry 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 minmar1eval
`|- ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( K ( Q ` M ) L ) J ) = 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 3 4 5 minmar1val
` |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( K ( Q ` M ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) )`
7 6 3expb
` |-  ( ( M e. B /\ ( K e. N /\ L e. N ) ) -> ( K ( Q ` M ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) )`
` |-  ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( K ( Q ` M ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) )`
9 simp3l
` |-  ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> I e. N )`
10 simpl3r
` |-  ( ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) /\ i = I ) -> J e. N )`
11 4 fvexi
` |-  .1. e. _V`
12 5 fvexi
` |-  .0. e. _V`
13 11 12 ifex
` |-  if ( j = L , .1. , .0. ) e. _V`
14 ovex
` |-  ( i M j ) e. _V`
15 13 14 ifex
` |-  if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) e. _V`
16 15 a1i
` |-  ( ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) e. _V )`
17 eqeq1
` |-  ( i = I -> ( i = K <-> I = K ) )`
` |-  ( ( i = I /\ j = J ) -> ( i = K <-> I = K ) )`
19 eqeq1
` |-  ( j = J -> ( j = L <-> J = L ) )`
` |-  ( ( i = I /\ j = J ) -> ( j = L <-> J = L ) )`
` |-  ( ( i = I /\ j = J ) -> if ( j = L , .1. , .0. ) = if ( J = L , .1. , .0. ) )`
` |-  ( ( i = I /\ j = J ) -> ( i M j ) = ( I M J ) )`
` |-  ( ( i = I /\ j = J ) -> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) = if ( I = K , if ( J = L , .1. , .0. ) , ( I M J ) ) )`
` |-  ( ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) = if ( I = K , if ( J = L , .1. , .0. ) , ( I M J ) ) )`
` |-  ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( ( K ( Q ` M ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) -> ( I ( K ( Q ` M ) L ) J ) = if ( I = K , if ( J = L , .1. , .0. ) , ( I M J ) ) ) )`
` |-  ( ( M e. B /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( K ( Q ` M ) L ) J ) = if ( I = K , if ( J = L , .1. , .0. ) , ( I M J ) ) )`