Theorem smattl

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

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		smattl.i	$$⊢\phi \to I\in \left(1..^K\right)$$
8		smattl.j	$$⊢\phi \to J\in \left(1..^L\right)$$
9		fzossnn	$$⊢\left(1..^K\right)\subseteq \mathbb{N}$$
10	9 7	sselid	$$⊢\phi \to I\in \mathbb{N}$$
11		fzossnn	$$⊢\left(1..^L\right)\subseteq \mathbb{N}$$
12	11 8	sselid	$$⊢\phi \to J\in \mathbb{N}$$
13		elfzolt2	$$⊢I\in \left(1..^K\right)\to I<K$$
14	7 13	syl	$$⊢\phi \to I<K$$
15	14	iftrued	$$⊢\phi \to if\left(I<K,I,I+1\right)=I$$
16		elfzolt2	$$⊢J\in \left(1..^L\right)\to J<L$$
17	8 16	syl	$$⊢\phi \to J<L$$
18	17	iftrued	$$⊢\phi \to if\left(J<L,J,J+1\right)=J$$
19	1 2 3 4 5 6 10 12 15 18	smatlem	$$⊢\phi \to ISJ=IAJ$$