Metamath Proof Explorer

Theorem smatfval

Description: Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Assertion smatfval ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → K subMat 1 ⁡ M L = M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1

Proof

Step Hyp Ref Expression
1 elex ⊢ M ∈ V → M ∈ V
2 1 3ad2ant3 ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → M ∈ V
3 coeq1 ⊢ m = M → m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 = M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
4 3 mpoeq3dv ⊢ m = M → k ∈ ℕ , l ∈ ℕ ⟼ m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 = k ∈ ℕ , l ∈ ℕ ⟼ M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
5 df-smat ⊢ subMat 1 = m ∈ V ⟼ k ∈ ℕ , l ∈ ℕ ⟼ m ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
6 nnex ⊢ ℕ ∈ V
7 6 6 mpoex ⊢ k ∈ ℕ , l ∈ ℕ ⟼ M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 ∈ V
8 4 5 7 fvmpt ⊢ M ∈ V → subMat 1 ⁡ M = k ∈ ℕ , l ∈ ℕ ⟼ M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
9 2 8 syl ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → subMat 1 ⁡ M = k ∈ ℕ , l ∈ ℕ ⟼ M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1
10 breq2 ⊢ k = K → i < k ↔ i < K
11 10 ifbid ⊢ k = K → if i < k i i + 1 = if i < K i i + 1
12 11 opeq1d ⊢ k = K → if i < k i i + 1 if j < l j j + 1 = if i < K i i + 1 if j < l j j + 1
13 12 mpoeq3dv ⊢ k = K → i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 = i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < l j j + 1
14 breq2 ⊢ l = L → j < l ↔ j < L
15 14 ifbid ⊢ l = L → if j < l j j + 1 = if j < L j j + 1
16 15 opeq2d ⊢ l = L → if i < K i i + 1 if j < l j j + 1 = if i < K i i + 1 if j < L j j + 1
17 16 mpoeq3dv ⊢ l = L → i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < l j j + 1 = i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
18 13 17 sylan9eq ⊢ k = K ∧ l = L → i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 = i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
19 18 adantl ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V ∧ k = K ∧ l = L → i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 = i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
20 19 coeq2d ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V ∧ k = K ∧ l = L → M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < k i i + 1 if j < l j j + 1 = M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
21 simp1 ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → K ∈ ℕ
22 simp2 ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → L ∈ ℕ
23 simp3 ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → M ∈ V
24 6 6 mpoex ⊢ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ∈ V
25 24 a1i ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ∈ V
26 coexg ⊢ M ∈ V ∧ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ∈ V → M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ∈ V
27 23 25 26 syl2anc ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ∈ V
28 9 20 21 22 27 ovmpod ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ M ∈ V → K subMat 1 ⁡ M L = M ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1