Metamath Proof Explorer

Theorem submatres

Description: Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 submat1n.a 
 |-  A = ( ( 1 ... N ) Mat R )
2 submat1n.b 
 |-  B = ( Base ` A )
3 1 2 submat1n 
 |-  ( ( N e. NN /\ M e. B ) -> ( N ( subMat1 ` M ) N ) = ( N ( ( ( 1 ... N ) subMat R ) ` M ) N ) )
4 simpr 
 |-  ( ( N e. NN /\ M e. B ) -> M e. B )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 5 eleq2i 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
7 6 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
8 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
9 7 8 syl 
 |-  ( N e. NN -> N e. ( 1 ... N ) )
10 9 adantr 
 |-  ( ( N e. NN /\ M e. B ) -> N e. ( 1 ... N ) )
11 eqid 
 |-  ( ( 1 ... N ) subMat R ) = ( ( 1 ... N ) subMat R )
12 1 11 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 ) ) )
13 4 10 10 12 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 ) ) )
14 fzdif2 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
15 7 14 syl 
 |-  ( N e. NN -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
16 difss 
 |-  ( ( 1 ... N ) \ { N } ) C_ ( 1 ... N )
17 15 16 eqsstrrdi 
 |-  ( N e. NN -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
18 17 adantr 
 |-  ( ( N e. NN /\ M e. B ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
19 resmpo 
 |-  ( ( ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) /\ ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) ) -> ( ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( i M j ) ) |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i M j ) ) )
20 18 18 19 syl2anc 
 |-  ( ( N e. NN /\ M e. B ) -> ( ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( i M j ) ) |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) = ( i e. ( 1 ... ( N - 1 ) ) , j e. ( 1 ... ( N - 1 ) ) |-> ( i M j ) ) )
21 1 2 matmpo 
 |-  ( M e. B -> M = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( i M j ) ) )
22 21 reseq1d 
 |-  ( M e. B -> ( M |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) = ( ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( i M j ) ) |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
23 22 adantl 
 |-  ( ( N e. NN /\ M e. B ) -> ( M |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) = ( ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( i M j ) ) |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
24 15 adantr 
 |-  ( ( N e. NN /\ M e. B ) -> ( ( 1 ... N ) \ { N } ) = ( 1 ... ( N - 1 ) ) )
25 eqidd 
 |-  ( ( N e. NN /\ M e. B ) -> ( i M j ) = ( i M j ) )
26 24 24 25 mpoeq123dv 
 |-  ( ( 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 M j ) ) )
27 20 23 26 3eqtr4rd 
 |-  ( ( N e. NN /\ M e. B ) -> ( i e. ( ( 1 ... N ) \ { N } ) , j e. ( ( 1 ... N ) \ { N } ) |-> ( i M j ) ) = ( M |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
28 3 13 27 3eqtrd 
 |-  ( ( N e. NN /\ M e. B ) -> ( N ( subMat1 ` M ) N ) = ( M |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )