Theorem smatbr

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

	Ref	Expression
Hypotheses	smat.s	⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
	smat.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	smat.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	smat.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑀 ) )
	smat.l	⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
	smat.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
	smatbr.i	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐾 ... 𝑀 ) )
	smatbr.j	⊢ ( 𝜑 → 𝐽 ∈ ( 𝐿 ... 𝑁 ) )
Assertion	smatbr	⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( ( 𝐼 + 1 ) 𝐴 ( 𝐽 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		smat.s	⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝐴 ) 𝐿 )
2		smat.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3		smat.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		smat.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑀 ) )
5		smat.l	⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
6		smat.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑m ( ( 1 ... 𝑀 ) × ( 1 ... 𝑁 ) ) ) )
7		smatbr.i	⊢ ( 𝜑 → 𝐼 ∈ ( 𝐾 ... 𝑀 ) )
8		smatbr.j	⊢ ( 𝜑 → 𝐽 ∈ ( 𝐿 ... 𝑁 ) )
9		fz1ssnn	⊢ ( 1 ... 𝑀 ) ⊆ ℕ
10	9 4	sselid	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
11		fzssnn	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 ... 𝑀 ) ⊆ ℕ )
12	10 11	syl	⊢ ( 𝜑 → ( 𝐾 ... 𝑀 ) ⊆ ℕ )
13	12 7	sseldd	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
14		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
15	14 5	sselid	⊢ ( 𝜑 → 𝐿 ∈ ℕ )
16		fzssnn	⊢ ( 𝐿 ∈ ℕ → ( 𝐿 ... 𝑁 ) ⊆ ℕ )
17	15 16	syl	⊢ ( 𝜑 → ( 𝐿 ... 𝑁 ) ⊆ ℕ )
18	17 8	sseldd	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
19		elfzle1	⊢ ( 𝐼 ∈ ( 𝐾 ... 𝑀 ) → 𝐾 ≤ 𝐼 )
20	7 19	syl	⊢ ( 𝜑 → 𝐾 ≤ 𝐼 )
21	10	nnred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
22	13	nnred	⊢ ( 𝜑 → 𝐼 ∈ ℝ )
23	21 22	lenltd	⊢ ( 𝜑 → ( 𝐾 ≤ 𝐼 ↔ ¬ 𝐼 < 𝐾 ) )
24	20 23	mpbid	⊢ ( 𝜑 → ¬ 𝐼 < 𝐾 )
25	24	iffalsed	⊢ ( 𝜑 → if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) = ( 𝐼 + 1 ) )
26		elfzle1	⊢ ( 𝐽 ∈ ( 𝐿 ... 𝑁 ) → 𝐿 ≤ 𝐽 )
27	8 26	syl	⊢ ( 𝜑 → 𝐿 ≤ 𝐽 )
28	15	nnred	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
29	18	nnred	⊢ ( 𝜑 → 𝐽 ∈ ℝ )
30	28 29	lenltd	⊢ ( 𝜑 → ( 𝐿 ≤ 𝐽 ↔ ¬ 𝐽 < 𝐿 ) )
31	27 30	mpbid	⊢ ( 𝜑 → ¬ 𝐽 < 𝐿 )
32	31	iffalsed	⊢ ( 𝜑 → if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) = ( 𝐽 + 1 ) )
33	1 2 3 4 5 6 13 18 25 32	smatlem	⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( ( 𝐼 + 1 ) 𝐴 ( 𝐽 + 1 ) ) )