smatbr

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

Step	Hyp	Ref	Expression
1		smat.s	$⊢ S = K {subMat}_{1} (A) L$
2		smat.m	$⊢ φ \to M \in ℕ$
3		smat.n	$⊢ φ \to N \in ℕ$
4		smat.k	$⊢ φ \to K \in (1 \dots M)$
5		smat.l	$⊢ φ \to L \in (1 \dots N)$
6		smat.a	$⊢ φ \to A \in (B^{((1 \dots M) \times (1 \dots N))})$
7		smatbr.i	$⊢ φ \to I \in (K \dots M)$
8		smatbr.j	$⊢ φ \to J \in (L \dots N)$
9		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
10	9 4	sselid	$⊢ φ \to K \in ℕ$
11		fzssnn	$⊢ K \in ℕ \to (K \dots M) \subseteq ℕ$
12	10 11	syl	$⊢ φ \to (K \dots M) \subseteq ℕ$
13	12 7	sseldd	$⊢ φ \to I \in ℕ$
14		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
15	14 5	sselid	$⊢ φ \to L \in ℕ$
16		fzssnn	$⊢ L \in ℕ \to (L \dots N) \subseteq ℕ$
17	15 16	syl	$⊢ φ \to (L \dots N) \subseteq ℕ$
18	17 8	sseldd	$⊢ φ \to J \in ℕ$
19		elfzle1	$⊢ I \in (K \dots M) \to K \leq I$
20	7 19	syl	$⊢ φ \to K \leq I$
21	10	nnred	$⊢ φ \to K \in ℝ$
22	13	nnred	$⊢ φ \to I \in ℝ$
23	21 22	lenltd	$⊢ φ \to (K \leq I \leftrightarrow \neg I < K)$
24	20 23	mpbid	$⊢ φ \to \neg I < K$
25	24	iffalsed	$⊢ φ \to if (I < K, I, I + 1) = I + 1$
26		elfzle1	$⊢ J \in (L \dots N) \to L \leq J$
27	8 26	syl	$⊢ φ \to L \leq J$
28	15	nnred	$⊢ φ \to L \in ℝ$
29	18	nnred	$⊢ φ \to J \in ℝ$
30	28 29	lenltd	$⊢ φ \to (L \leq J \leftrightarrow \neg J < L)$
31	27 30	mpbid	$⊢ φ \to \neg J < L$
32	31	iffalsed	$⊢ φ \to if (J < L, J, J + 1) = J + 1$
33	1 2 3 4 5 6 13 18 25 32	smatlem	$⊢ φ \to I S J = (I + 1) A (J + 1)$

Metamath Proof Explorer