Metamath Proof Explorer


Theorem smatbl

Description: Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Hypotheses smat.s 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
smat.m ( 𝜑𝑀 ∈ ℕ )
smat.n ( 𝜑𝑁 ∈ ℕ )
smat.k ( 𝜑𝐾 ∈ ( 1 ... 𝑀 ) )
smat.l ( 𝜑𝐿 ∈ ( 1 ... 𝑁 ) )
smat.a ( 𝜑𝐴 ∈ ( 𝐵m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
smatbl.i ( 𝜑𝐼 ∈ ( 1 ..^ 𝐾 ) )
smatbl.j ( 𝜑𝐽 ∈ ( 𝐿 ... 𝑁 ) )
Assertion smatbl ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝐼 𝐴 ( 𝐽 + 1 ) ) )

Proof

Step Hyp Ref Expression
1 smat.s 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
2 smat.m ( 𝜑𝑀 ∈ ℕ )
3 smat.n ( 𝜑𝑁 ∈ ℕ )
4 smat.k ( 𝜑𝐾 ∈ ( 1 ... 𝑀 ) )
5 smat.l ( 𝜑𝐿 ∈ ( 1 ... 𝑁 ) )
6 smat.a ( 𝜑𝐴 ∈ ( 𝐵m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
7 smatbl.i ( 𝜑𝐼 ∈ ( 1 ..^ 𝐾 ) )
8 smatbl.j ( 𝜑𝐽 ∈ ( 𝐿 ... 𝑁 ) )
9 fzossnn ( 1 ..^ 𝐾 ) ⊆ ℕ
10 9 7 sselid ( 𝜑𝐼 ∈ ℕ )
11 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
12 11 5 sselid ( 𝜑𝐿 ∈ ℕ )
13 fzssnn ( 𝐿 ∈ ℕ → ( 𝐿 ... 𝑁 ) ⊆ ℕ )
14 12 13 syl ( 𝜑 → ( 𝐿 ... 𝑁 ) ⊆ ℕ )
15 14 8 sseldd ( 𝜑𝐽 ∈ ℕ )
16 elfzolt2 ( 𝐼 ∈ ( 1 ..^ 𝐾 ) → 𝐼 < 𝐾 )
17 7 16 syl ( 𝜑𝐼 < 𝐾 )
18 17 iftrued ( 𝜑 → if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) = 𝐼 )
19 elfzle1 ( 𝐽 ∈ ( 𝐿 ... 𝑁 ) → 𝐿𝐽 )
20 8 19 syl ( 𝜑𝐿𝐽 )
21 12 nnred ( 𝜑𝐿 ∈ ℝ )
22 15 nnred ( 𝜑𝐽 ∈ ℝ )
23 21 22 lenltd ( 𝜑 → ( 𝐿𝐽 ↔ ¬ 𝐽 < 𝐿 ) )
24 20 23 mpbid ( 𝜑 → ¬ 𝐽 < 𝐿 )
25 24 iffalsed ( 𝜑 → if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) = ( 𝐽 + 1 ) )
26 1 2 3 4 5 6 10 15 18 25 smatlem ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝐼 𝐴 ( 𝐽 + 1 ) ) )