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

Proof

Step Hyp Ref Expression
1 submat1n.a ⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
2 submat1n.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 1 2 submat1n ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) )
4 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
5 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
6 5 eleq2i ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
7 6 biimpi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
8 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
9 7 8 syl ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 ... 𝑁 ) )
10 9 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
11 eqid ⊢ ( ( 1 ... 𝑁 ) subMat 𝑅 ) = ( ( 1 ... 𝑁 ) subMat 𝑅 )
12 1 11 2 submaval ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ∧ 𝑁 ∈ ( 1 ... 𝑁 ) ) → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) = ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
13 4 10 10 12 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ( ( ( 1 ... 𝑁 ) subMat 𝑅 ) ‘ 𝑀 ) 𝑁 ) = ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
14 fzdif2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
15 7 14 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
16 difss ⊢ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ⊆ ( 1 ... 𝑁 )
17 15 16 eqsstrrdi ⊢ ( 𝑁 ∈ ℕ → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
18 17 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
19 resmpo ⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) ∧ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) ) → ( ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑖 𝑀 𝑗 ) ) ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
20 18 18 19 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑖 𝑀 𝑗 ) ) ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
21 1 2 matmpo ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 = ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
22 21 reseq1d ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑀 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑖 𝑀 𝑗 ) ) ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
23 22 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( ( 𝑖 ∈ ( 1 ... 𝑁 ) , 𝑗 ∈ ( 1 ... 𝑁 ) ↦ ( 𝑖 𝑀 𝑗 ) ) ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
24 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) = ( 1 ... ( 𝑁 − 1 ) ) )
25 eqidd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
26 24 24 25 mpoeq123dv ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑖 ∈ ( 1 ... ( 𝑁 − 1 ) ) , 𝑗 ∈ ( 1 ... ( 𝑁 − 1 ) ) ↦ ( 𝑖 𝑀 𝑗 ) ) )
27 20 23 26 3eqtr4rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) , 𝑗 ∈ ( ( 1 ... 𝑁 ) ∖ { 𝑁 } ) ↦ ( 𝑖 𝑀 𝑗 ) ) = ( 𝑀 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
28 3 13 27 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ( subMat1 ‘ 𝑀 ) 𝑁 ) = ( 𝑀 ↾ ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )