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→KsubMat1⁡ML=M∘i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+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∈ℕ⟼ifi<kii+1ifj<ljj+1=M∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
4 3 mpoeq3dv ⊢m=M→k∈ℕ,l∈ℕ⟼m∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1=k∈ℕ,l∈ℕ⟼M∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
5 df-smat ⊢subMat1=m∈V⟼k∈ℕ,l∈ℕ⟼m∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
6 nnex ⊢ℕ∈V
7 6 6 mpoex ⊢k∈ℕ,l∈ℕ⟼M∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1∈V
8 4 5 7 fvmpt ⊢M∈V→subMat1⁡M=k∈ℕ,l∈ℕ⟼M∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
9 2 8 syl ⊢K∈ℕ∧L∈ℕ∧M∈V→subMat1⁡M=k∈ℕ,l∈ℕ⟼M∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1
10 breq2 ⊢k=K→i<k↔i<K
11 10 ifbid ⊢k=K→ifi<kii+1=ifi<Kii+1
12 11 opeq1d ⊢k=K→ifi<kii+1ifj<ljj+1=ifi<Kii+1ifj<ljj+1
13 12 mpoeq3dv ⊢k=K→i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1=i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<ljj+1
14 breq2 ⊢l=L→j<l↔j<L
15 14 ifbid ⊢l=L→ifj<ljj+1=ifj<Ljj+1
16 15 opeq2d ⊢l=L→ifi<Kii+1ifj<ljj+1=ifi<Kii+1ifj<Ljj+1
17 16 mpoeq3dv ⊢l=L→i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<ljj+1=i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1
18 13 17 sylan9eq ⊢k=K∧l=L→i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1=i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1
19 18 adantl ⊢K∈ℕ∧L∈ℕ∧M∈V∧k=K∧l=L→i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1=i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1
20 19 coeq2d ⊢K∈ℕ∧L∈ℕ∧M∈V∧k=K∧l=L→M∘i∈ℕ,j∈ℕ⟼ifi<kii+1ifj<ljj+1=M∘i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+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∈ℕ⟼ifi<Kii+1ifj<Ljj+1∈V
25 24 a1i ⊢K∈ℕ∧L∈ℕ∧M∈V→i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1∈V
26 coexg ⊢M∈V∧i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1∈V→M∘i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1∈V
27 23 25 26 syl2anc ⊢K∈ℕ∧L∈ℕ∧M∈V→M∘i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1∈V
28 9 20 21 22 27 ovmpod ⊢K∈ℕ∧L∈ℕ∧M∈V→KsubMat1⁡ML=M∘i∈ℕ,j∈ℕ⟼ifi<Kii+1ifj<Ljj+1