# Metamath Proof Explorer

## Theorem minmar1val

Description: Third 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 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 ) ) ) )`

### 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 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 ) ) ) ) )`
` |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( 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 ) ) ) ) )`
8 simp2
` |-  ( ( M e. B /\ K e. N /\ L e. N ) -> K e. N )`
9 simpl3
` |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ k = K ) -> L e. N )`
10 1 2 matrcl
` |-  ( M e. B -> ( N e. Fin /\ R e. _V ) )`
11 10 simpld
` |-  ( M e. B -> N e. Fin )`
12 11 11 jca
` |-  ( M e. B -> ( N e. Fin /\ N e. Fin ) )`
` |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( N e. Fin /\ N e. Fin ) )`
` |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ ( k = K /\ l = L ) ) -> ( N e. Fin /\ N e. Fin ) )`
15 mpoexga
` |-  ( ( N e. Fin /\ N e. Fin ) -> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) e. _V )`
16 14 15 syl
` |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ ( k = K /\ l = L ) ) -> ( i e. N , j e. N |-> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) ) e. _V )`
17 eqeq2
` |-  ( k = K -> ( i = k <-> i = K ) )`
` |-  ( ( k = K /\ l = L ) -> ( i = k <-> i = K ) )`
19 eqeq2
` |-  ( l = L -> ( j = l <-> j = L ) )`
20 19 ifbid
` |-  ( l = L -> if ( j = l , .1. , .0. ) = if ( j = L , .1. , .0. ) )`
` |-  ( ( k = K /\ l = L ) -> if ( j = l , .1. , .0. ) = if ( j = L , .1. , .0. ) )`
` |-  ( ( k = K /\ l = L ) -> if ( i = k , if ( j = l , .1. , .0. ) , ( i M j ) ) = if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) )`
` |-  ( ( k = K /\ l = L ) -> ( 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 ) ) ) )`
` |-  ( ( ( M e. B /\ K e. N /\ L e. N ) /\ ( k = K /\ l = L ) ) -> ( 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 ) ) ) )`
` |-  ( ( M e. B /\ K e. N /\ L e. N ) -> ( ( 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 ) ) ) ) -> ( 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 ) -> ( K ( Q ` M ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , .1. , .0. ) , ( i M j ) ) ) )`