# Metamath Proof Explorer

## Theorem submat1n

Description: One case where the submatrix with integer indices, subMat1 , and the general submatrix subMat , agree. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses submat1n.a
`|- A = ( ( 1 ... N ) Mat R )`
submat1n.b
`|- B = ( Base ` A )`
Assertion submat1n
`|- ( ( N e. NN /\ M e. B ) -> ( N ( subMat1 ` M ) N ) = ( N ( ( ( 1 ... N ) subMat R ) ` M ) N ) )`

### Proof

Step Hyp Ref Expression
1 submat1n.a
` |-  A = ( ( 1 ... N ) Mat R )`
2 submat1n.b
` |-  B = ( Base ` A )`
3 fzdif2
` |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )`
4 nnuz
` |-  NN = ( ZZ>= ` 1 )`
5 3 4 eleq2s
` |-  ( N e. NN -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )`
6 5 adantr
` |-  ( ( N e. NN /\ M e. B ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )`
7 6 adantr
` |-  ( ( ( N e. NN /\ M e. B ) /\ i e. ( ( 1 ... N ) \ { N } ) ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )`
8 eqid
` |-  ( N ( subMat1 ` M ) N ) = ( N ( subMat1 ` M ) N )`
9 elfz1end
` |-  ( N e. NN <-> N e. ( 1 ... N ) )`
10 9 biimpi
` |-  ( N e. NN -> N e. ( 1 ... N ) )`
11 10 adantr
` |-  ( ( N e. NN /\ M e. B ) -> N e. ( 1 ... N ) )`
12 11 9 sylibr
` |-  ( ( N e. NN /\ M e. B ) -> N e. NN )`
13 12 adantr
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> N e. NN )`
14 13 10 syl
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> N e. ( 1 ... N ) )`
15 eqid
` |-  ( Base ` R ) = ( Base ` R )`
16 1 15 2 matbas2i
` |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )`
17 16 ad2antlr
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> M e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )`
18 simprl
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> i e. ( ( 1 ... N ) \ { N } ) )`
19 nnz
` |-  ( N e. NN -> N e. ZZ )`
20 fzoval
` |-  ( N e. ZZ -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )`
21 19 20 syl
` |-  ( N e. NN -> ( 1 ..^ N ) = ( 1 ... ( N - 1 ) ) )`
22 21 5 eqtr4d
` |-  ( N e. NN -> ( 1 ..^ N ) = ( ( 1 ... N ) \ { N } ) )`
23 13 22 syl
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> ( 1 ..^ N ) = ( ( 1 ... N ) \ { N } ) )`
24 18 23 eleqtrrd
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> i e. ( 1 ..^ N ) )`
25 simprr
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> j e. ( ( 1 ... N ) \ { N } ) )`
26 25 23 eleqtrrd
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> j e. ( 1 ..^ N ) )`
27 8 13 13 14 14 17 24 26 smattl
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> ( i ( N ( subMat1 ` M ) N ) j ) = ( i M j ) )`
28 27 eqcomd
` |-  ( ( ( N e. NN /\ M e. B ) /\ ( i e. ( ( 1 ... N ) \ { N } ) /\ j e. ( ( 1 ... N ) \ { N } ) ) ) -> ( i M j ) = ( i ( N ( subMat1 ` M ) N ) j ) )`
29 6 7 28 mpoeq123dva
` |-  ( ( N e. NN /\ M e. B ) -> ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i M j ) ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i ( N ( subMat1 ` M ) N ) j ) ) )`
30 simpr
` |-  ( ( N e. NN /\ M e. B ) -> M e. B )`
31 eqid
` |-  ( ( 1 ... N ) subMat R ) = ( ( 1 ... N ) subMat R )`
32 1 31 2 submaval
` |-  ( ( M e. B /\ N e. ( 1 ... N ) /\ N e. ( 1 ... N ) ) -> ( N ( ( ( 1 ... N ) subMat R ) ` M ) N ) = ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i M j ) ) )`
33 30 11 11 32 syl3anc
` |-  ( ( N e. NN /\ M e. B ) -> ( N ( ( ( 1 ... N ) subMat R ) ` M ) N ) = ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i M j ) ) )`
34 eqid
` |-  ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )`
35 1 2 34 8 12 11 11 30 smatcl
` |-  ( ( N e. NN /\ M e. B ) -> ( N ( subMat1 ` M ) N ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )`
36 eqid
` |-  ( ( 1 ... ( N - 1 ) ) Mat R ) = ( ( 1 ... ( N - 1 ) ) Mat R )`
37 36 34 matmpo
` |-  ( ( N ( subMat1 ` M ) N ) e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) -> ( N ( subMat1 ` M ) N ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i ( N ( subMat1 ` M ) N ) j ) ) )`
38 35 37 syl
` |-  ( ( N e. NN /\ M e. B ) -> ( N ( subMat1 ` M ) N ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i ( N ( subMat1 ` M ) N ) j ) ) )`
39 29 33 38 3eqtr4rd
` |-  ( ( N e. NN /\ M e. B ) -> ( N ( subMat1 ` M ) N ) = ( N ( ( ( 1 ... N ) subMat R ) ` M ) N ) )`