Theorem smatbr

Description: Entries of a submatrix, bottom 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 ) ) ) )
	smatbr.i	|- ( ph -> I e. ( K ... M ) )
	smatbr.j	|- ( ph -> J e. ( L ... N ) )
Assertion	smatbr	|- ( ph -> ( I S J ) = ( ( I + 1 ) A ( J + 1 ) ) )

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		smatbr.i	|- ( ph -> I e. ( K ... M ) )
8		smatbr.j	|- ( ph -> J e. ( L ... N ) )
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		fz1ssnn	|- ( 1 ... N ) C_ NN
15	14 5	sselid	|- ( ph -> L e. NN )
16		fzssnn	|- ( L e. NN -> ( L ... N ) C_ NN )
17	15 16	syl	|- ( ph -> ( L ... N ) C_ NN )
18	17 8	sseldd	|- ( ph -> J e. NN )
19		elfzle1	|- ( I e. ( K ... M ) -> K <_ I )
20	7 19	syl	|- ( ph -> K <_ I )
21	10	nnred	|- ( ph -> K e. RR )
22	13	nnred	|- ( ph -> I e. RR )
23	21 22	lenltd	|- ( ph -> ( K <_ I <-> -. I < K ) )
24	20 23	mpbid	|- ( ph -> -. I < K )
25	24	iffalsed	|- ( ph -> if ( I < K , I , ( I + 1 ) ) = ( I + 1 ) )
26		elfzle1	|- ( J e. ( L ... N ) -> L <_ J )
27	8 26	syl	|- ( ph -> L <_ J )
28	15	nnred	|- ( ph -> L e. RR )
29	18	nnred	|- ( ph -> J e. RR )
30	28 29	lenltd	|- ( ph -> ( L <_ J <-> -. J < L ) )
31	27 30	mpbid	|- ( ph -> -. J < L )
32	31	iffalsed	|- ( ph -> if ( J < L , J , ( J + 1 ) ) = ( J + 1 ) )
33	1 2 3 4 5 6 13 18 25 32	smatlem	|- ( ph -> ( I S J ) = ( ( I + 1 ) A ( J + 1 ) ) )