# Metamath Proof Explorer

## 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 ℕ$
smat.n ${⊢}{\phi }\to {N}\in ℕ$
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)×\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 {I}{S}{J}={I}{A}{J}$

### Proof

Step Hyp Ref Expression
1 smat.s ${⊢}{S}={K}{\mathrm{subMat}}_{1}\left({A}\right){L}$
2 smat.m ${⊢}{\phi }\to {M}\in ℕ$
3 smat.n ${⊢}{\phi }\to {N}\in ℕ$
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)×\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 ℕ$
10 9 7 sseldi ${⊢}{\phi }\to {I}\in ℕ$
11 fzossnn ${⊢}\left(1..^{L}\right)\subseteq ℕ$
12 11 8 sseldi ${⊢}{\phi }\to {J}\in ℕ$
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 {I}{S}{J}={I}{A}{J}$