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 ) )