Theorem smattl

Description: Entries of a submatrix, top left. (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 ) ) ) )
	smattl.i	|- ( ph -> I e. ( 1 ..^ K ) )
	smattl.j	|- ( ph -> J e. ( 1 ..^ L ) )
Assertion	smattl	|- ( ph -> ( I S J ) = ( I 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		smattl.i	|- ( ph -> I e. ( 1 ..^ K ) )
8		smattl.j	|- ( ph -> J e. ( 1 ..^ L ) )
9		fzossnn	|- ( 1 ..^ K ) C_ NN
10	9 7	sseldi	|- ( ph -> I e. NN )
11		fzossnn	|- ( 1 ..^ L ) C_ NN
12	11 8	sseldi	|- ( ph -> J e. NN )
13		elfzolt2	|- ( I e. ( 1 ..^ K ) -> I < K )
14	7 13	syl	|- ( ph -> I < K )
15	14	iftrued	|- ( ph -> if ( I < K , I , ( I + 1 ) ) = I )
16		elfzolt2	|- ( J e. ( 1 ..^ L ) -> J < L )
17	8 16	syl	|- ( ph -> J < L )
18	17	iftrued	|- ( ph -> if ( J < L , J , ( J + 1 ) ) = J )
19	1 2 3 4 5 6 10 12 15 18	smatlem	|- ( ph -> ( I S J ) = ( I A J ) )