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 𝑅 ) ‘ 𝑀 ) 𝑁 ) )