Theorem smatbl

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

	Ref	Expression
Hypotheses	smat.s	$$⊢S=K{\mathrm{subMat}}_1\left(A\right)L$$
	smat.m	$$⊢\phi \to M\in \mathbb{N}$$
	smat.n	$$⊢\phi \to N\in \mathbb{N}$$
	smat.k	$$⊢\phi \to K\in \left(1\dots M\right)$$
	smat.l	$$⊢\phi \to L\in \left(1\dots N\right)$$
	smat.a	$$⊢\phi \to A\in \left(B^{\left(\left(1\dots M\right)\times \left(1\dots N\right)\right)}\right)$$
	smatbl.i	$$⊢\phi \to I\in \left(1..^K\right)$$
	smatbl.j	$$⊢\phi \to J\in \left(L\dots N\right)$$
Assertion	smatbl	$$⊢\phi \to ISJ=IA\left(J+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		smat.s	$$⊢S=K{\mathrm{subMat}}_1\left(A\right)L$$
2		smat.m	$$⊢\phi \to M\in \mathbb{N}$$
3		smat.n	$$⊢\phi \to N\in \mathbb{N}$$
4		smat.k	$$⊢\phi \to K\in \left(1\dots M\right)$$
5		smat.l	$$⊢\phi \to L\in \left(1\dots N\right)$$
6		smat.a	$$⊢\phi \to A\in \left(B^{\left(\left(1\dots M\right)\times \left(1\dots N\right)\right)}\right)$$
7		smatbl.i	$$⊢\phi \to I\in \left(1..^K\right)$$
8		smatbl.j	$$⊢\phi \to J\in \left(L\dots N\right)$$
9		fzossnn	$$⊢\left(1..^K\right)\subseteq \mathbb{N}$$
10	9 7	sseldi	$$⊢\phi \to I\in \mathbb{N}$$
11		fz1ssnn	$$⊢\left(1\dots N\right)\subseteq \mathbb{N}$$
12	11 5	sseldi	$$⊢\phi \to L\in \mathbb{N}$$
13		fzssnn	$$⊢L\in \mathbb{N}\to \left(L\dots N\right)\subseteq \mathbb{N}$$
14	12 13	syl	$$⊢\phi \to \left(L\dots N\right)\subseteq \mathbb{N}$$
15	14 8	sseldd	$$⊢\phi \to J\in \mathbb{N}$$
16		elfzolt2	$$⊢I\in \left(1..^K\right)\to I<K$$
17	7 16	syl	$$⊢\phi \to I<K$$
18	17	iftrued	$$⊢\phi \to if\left(I<K,I,I+1\right)=I$$
19		elfzle1	$$⊢J\in \left(L\dots N\right)\to L\le J$$
20	8 19	syl	$$⊢\phi \to L\le J$$
21	12	nnred	$$⊢\phi \to L\in ℝ$$
22	15	nnred	$$⊢\phi \to J\in ℝ$$
23	21 22	lenltd	$$⊢\phi \to \left(L\le J\leftrightarrow \neg J<L\right)$$
24	20 23	mpbid	$$⊢\phi \to \neg J<L$$
25	24	iffalsed	$$⊢\phi \to if\left(J<L,J,J+1\right)=J+1$$
26	1 2 3 4 5 6 10 15 18 25	smatlem	$$⊢\phi \to ISJ=IA\left(J+1\right)$$