Theorem smattl

Description: Entries of a submatrix, top left. (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 ... 𝑁 ) ) ) )
	smattl.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ..^ 𝐾 ) )
	smattl.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ..^ 𝐿 ) )
Assertion	smattl	⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝐼 𝐴 𝐽 ) )

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		smattl.i	⊢ ( 𝜑 → 𝐼 ∈ ( 1 ..^ 𝐾 ) )
8		smattl.j	⊢ ( 𝜑 → 𝐽 ∈ ( 1 ..^ 𝐿 ) )
9		fzossnn	⊢ ( 1 ..^ 𝐾 ) ⊆ ℕ
10	9 7	sselid	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
11		fzossnn	⊢ ( 1 ..^ 𝐿 ) ⊆ ℕ
12	11 8	sselid	⊢ ( 𝜑 → 𝐽 ∈ ℕ )
13		elfzolt2	⊢ ( 𝐼 ∈ ( 1 ..^ 𝐾 ) → 𝐼 < 𝐾 )
14	7 13	syl	⊢ ( 𝜑 → 𝐼 < 𝐾 )
15	14	iftrued	⊢ ( 𝜑 → if ( 𝐼 < 𝐾 , 𝐼 , ( 𝐼 + 1 ) ) = 𝐼 )
16		elfzolt2	⊢ ( 𝐽 ∈ ( 1 ..^ 𝐿 ) → 𝐽 < 𝐿 )
17	8 16	syl	⊢ ( 𝜑 → 𝐽 < 𝐿 )
18	17	iftrued	⊢ ( 𝜑 → if ( 𝐽 < 𝐿 , 𝐽 , ( 𝐽 + 1 ) ) = 𝐽 )
19	1 2 3 4 5 6 10 12 15 18	smatlem	⊢ ( 𝜑 → ( 𝐼 𝑆 𝐽 ) = ( 𝐼 𝐴 𝐽 ) )