Metamath Proof Explorer


Theorem smattr

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

Ref Expression
Hypotheses smat.s
|- S = ( K ( subMat1 ` A ) L )
smat.m
|- ( ph -> M e. NN )
smat.n
|- ( ph -> N e. NN )
smat.k
|- ( ph -> K e. ( 1 ... M ) )
smat.l
|- ( ph -> L e. ( 1 ... N ) )
smat.a
|- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
smattr.i
|- ( ph -> I e. ( K ... M ) )
smattr.j
|- ( ph -> J e. ( 1 ..^ L ) )
Assertion smattr
|- ( ph -> ( I S J ) = ( ( I + 1 ) A J ) )

Proof

Step Hyp Ref Expression
1 smat.s
 |-  S = ( K ( subMat1 ` A ) L )
2 smat.m
 |-  ( ph -> M e. NN )
3 smat.n
 |-  ( ph -> N e. NN )
4 smat.k
 |-  ( ph -> K e. ( 1 ... M ) )
5 smat.l
 |-  ( ph -> L e. ( 1 ... N ) )
6 smat.a
 |-  ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )
7 smattr.i
 |-  ( ph -> I e. ( K ... M ) )
8 smattr.j
 |-  ( ph -> J e. ( 1 ..^ L ) )
9 fz1ssnn
 |-  ( 1 ... M ) C_ NN
10 9 4 sselid
 |-  ( ph -> K e. NN )
11 fzssnn
 |-  ( K e. NN -> ( K ... M ) C_ NN )
12 10 11 syl
 |-  ( ph -> ( K ... M ) C_ NN )
13 12 7 sseldd
 |-  ( ph -> I e. NN )
14 fzossnn
 |-  ( 1 ..^ L ) C_ NN
15 14 8 sselid
 |-  ( ph -> J e. NN )
16 elfzle1
 |-  ( I e. ( K ... M ) -> K <_ I )
17 7 16 syl
 |-  ( ph -> K <_ I )
18 10 nnred
 |-  ( ph -> K e. RR )
19 13 nnred
 |-  ( ph -> I e. RR )
20 18 19 lenltd
 |-  ( ph -> ( K <_ I <-> -. I < K ) )
21 17 20 mpbid
 |-  ( ph -> -. I < K )
22 21 iffalsed
 |-  ( ph -> if ( I < K , I , ( I + 1 ) ) = ( I + 1 ) )
23 elfzolt2
 |-  ( J e. ( 1 ..^ L ) -> J < L )
24 8 23 syl
 |-  ( ph -> J < L )
25 24 iftrued
 |-  ( ph -> if ( J < L , J , ( J + 1 ) ) = J )
26 1 2 3 4 5 6 13 15 22 25 smatlem
 |-  ( ph -> ( I S J ) = ( ( I + 1 ) A J ) )