Theorem smattr

Description: Entries of a submatrix, top right. (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)$$
	smattr.i	$$⊢\phi \to I\in \left(K\dots M\right)$$
	smattr.j	$$⊢\phi \to J\in \left(1..^L\right)$$
Assertion	smattr	$$⊢\phi \to ISJ=\left(I+1\right)AJ$$

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		smattr.i	$$⊢\phi \to I\in \left(K\dots M\right)$$
8		smattr.j	$$⊢\phi \to J\in \left(1..^L\right)$$
9		fz1ssnn	$$⊢\left(1\dots M\right)\subseteq \mathbb{N}$$
10	9 4	sseldi	$$⊢\phi \to K\in \mathbb{N}$$
11		fzssnn	$$⊢K\in \mathbb{N}\to \left(K\dots M\right)\subseteq \mathbb{N}$$
12	10 11	syl	$$⊢\phi \to \left(K\dots M\right)\subseteq \mathbb{N}$$
13	12 7	sseldd	$$⊢\phi \to I\in \mathbb{N}$$
14		fzossnn	$$⊢\left(1..^L\right)\subseteq \mathbb{N}$$
15	14 8	sseldi	$$⊢\phi \to J\in \mathbb{N}$$
16		elfzle1	$$⊢I\in \left(K\dots M\right)\to K\le I$$
17	7 16	syl	$$⊢\phi \to K\le I$$
18	10	nnred	$$⊢\phi \to K\in ℝ$$
19	13	nnred	$$⊢\phi \to I\in ℝ$$
20	18 19	lenltd	$$⊢\phi \to \left(K\le I\leftrightarrow \neg I<K\right)$$
21	17 20	mpbid	$$⊢\phi \to \neg I<K$$
22	21	iffalsed	$$⊢\phi \to if\left(I<K,I,I+1\right)=I+1$$
23		elfzolt2	$$⊢J\in \left(1..^L\right)\to J<L$$
24	8 23	syl	$$⊢\phi \to J<L$$
25	24	iftrued	$$⊢\phi \to if\left(J<L,J,J+1\right)=J$$
26	1 2 3 4 5 6 13 15 22 25	smatlem	$$⊢\phi \to ISJ=\left(I+1\right)AJ$$