# 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 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
submat1n.b 𝐵 = ( Base ‘ 𝐴 )
Assertion submat1n ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) )

### Proof

Step Hyp Ref Expression
1 submat1n.a 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
2 submat1n.b 𝐵 = ( Base ‘ 𝐴 )
3 fzdif2 ( 𝑁 ∈ ( ℤ ‘ 1 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
4 nnuz ℕ = ( ℤ ‘ 1 )
5 3 4 eleq2s ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
6 5 adantr ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
7 6 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
8 eqid ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 )
9 elfz1end ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( 1 ... 𝑁 ) )
10 9 biimpi ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... 𝑁 ) )
11 10 adantr ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
12 11 9 sylibr ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → 𝑁 ∈ ℕ )
13 12 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑁 ∈ ℕ )
14 13 10 syl ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
15 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 1 15 2 matbas2i ( 𝑀𝐵𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
17 16 ad2antlr ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
18 simprl ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) )
19 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
20 fzoval ( 𝑁 ∈ ℤ → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
21 19 20 syl ( 𝑁 ∈ ℕ → ( 1 ..^ 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
22 21 5 eqtr4d ( 𝑁 ∈ ℕ → ( 1 ..^ 𝑁 ) = ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) )
23 13 22 syl ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → ( 1 ..^ 𝑁 ) = ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) )
24 18 23 eleqtrrd ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑖 ∈ ( 1 ..^ 𝑁 ) )
25 simprr ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) )
26 25 23 eleqtrrd ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → 𝑗 ∈ ( 1 ..^ 𝑁 ) )
27 8 13 13 14 14 17 24 26 smattl ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → ( 𝑖 ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
28 27 eqcomd ( ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) ∧ ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ∧ 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ) ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) 𝑗 ) )
29 6 7 28 mpoeq123dva ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) 𝑗 ) ) )
30 simpr ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → 𝑀𝐵 )
31 eqid ( ( 1 ... 𝑁 ) subMat 𝑅 ) = ( ( 1 ... 𝑁 ) subMat 𝑅 )
32 1 31 2 submaval ( ( 𝑀𝐵𝑁 ∈ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) = ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
33 30 11 11 32 syl3anc ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) = ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
34 eqid ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
35 1 2 34 8 12 11 11 30 smatcl ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
36 eqid ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
37 36 34 matmpo ( ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) 𝑗 ) ) )
38 35 37 syl ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) 𝑗 ) ) )
39 29 33 38 3eqtr4rd ( ( 𝑁 ∈ ℕ ∧ 𝑀𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) )