Metamath Proof Explorer

Theorem smatlem

Description: Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Hypotheses smat.s ⊢ S = K subMat 1 ⁡ A L
smat.m ⊢ φ → M ∈ ℕ
smat.n ⊢ φ → N ∈ ℕ
smat.k ⊢ φ → K ∈ 1 … M
smat.l ⊢ φ → L ∈ 1 … N
smat.a ⊢ φ → A ∈ B 1 … M × 1 … N
smatlem.i ⊢ φ → I ∈ ℕ
smatlem.j ⊢ φ → J ∈ ℕ
smatlem.1 ⊢ φ → if I < K I I + 1 = X
smatlem.2 ⊢ φ → if J < L J J + 1 = Y
Assertion smatlem ⊢ φ → I S J = X A Y

Proof

Step Hyp Ref Expression
1 smat.s ⊢ S = K subMat 1 ⁡ A L
2 smat.m ⊢ φ → M ∈ ℕ
3 smat.n ⊢ φ → N ∈ ℕ
4 smat.k ⊢ φ → K ∈ 1 … M
5 smat.l ⊢ φ → L ∈ 1 … N
6 smat.a ⊢ φ → A ∈ B 1 … M × 1 … N
7 smatlem.i ⊢ φ → I ∈ ℕ
8 smatlem.j ⊢ φ → J ∈ ℕ
9 smatlem.1 ⊢ φ → if I < K I I + 1 = X
10 smatlem.2 ⊢ φ → if J < L J J + 1 = Y
11 fz1ssnn ⊢ 1 … M ⊆ ℕ
12 11 4 sseldi ⊢ φ → K ∈ ℕ
13 fz1ssnn ⊢ 1 … N ⊆ ℕ
14 13 5 sseldi ⊢ φ → L ∈ ℕ
15 smatfval ⊢ K ∈ ℕ ∧ L ∈ ℕ ∧ A ∈ B 1 … M × 1 … N → K subMat 1 ⁡ A L = A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
16 12 14 6 15 syl3anc ⊢ φ → K subMat 1 ⁡ A L = A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
17 1 16 syl5eq ⊢ φ → S = A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
18 17 oveqd ⊢ φ → I S J = I A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 J
19 df-ov ⊢ I A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 J = A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
20 18 19 syl6eq ⊢ φ → I S J = A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
21 7 8 jca ⊢ φ → I ∈ ℕ ∧ J ∈ ℕ
22 opelxp ⊢ I J ∈ ℕ × ℕ ↔ I ∈ ℕ ∧ J ∈ ℕ
23 21 22 sylibr ⊢ φ → I J ∈ ℕ × ℕ
24 eqid ⊢ 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
25 opex ⊢ if i < K i i + 1 if j < L j j + 1 ∈ V
26 24 25 dmmpo ⊢ dom ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 = ℕ × ℕ
27 23 26 eleqtrrdi ⊢ φ → I J ∈ dom ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
28 24 mpofun ⊢ Fun ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1
29 fvco ⊢ Fun ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ∧ I J ∈ dom ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 → A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J = A ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
30 28 29 mpan ⊢ I J ∈ dom ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 → A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J = A ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
31 27 30 syl ⊢ φ → A ∘ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J = A ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
32 20 31 eqtrd ⊢ φ → I S J = A ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
33 df-ov ⊢ I i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 J = i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J
34 breq1 ⊢ i = I → i < K ↔ I < K
35 id ⊢ i = I → i = I
36 oveq1 ⊢ i = I → i + 1 = I + 1
37 34 35 36 ifbieq12d ⊢ i = I → if i < K i i + 1 = if I < K I I + 1
38 37 opeq1d ⊢ i = I → if i < K i i + 1 if j < L j j + 1 = if I < K I I + 1 if j < L j j + 1
39 breq1 ⊢ j = J → j < L ↔ J < L
40 id ⊢ j = J → j = J
41 oveq1 ⊢ j = J → j + 1 = J + 1
42 39 40 41 ifbieq12d ⊢ j = J → if j < L j j + 1 = if J < L J J + 1
43 42 opeq2d ⊢ j = J → if I < K I I + 1 if j < L j j + 1 = if I < K I I + 1 if J < L J J + 1
44 opex ⊢ if I < K I I + 1 if J < L J J + 1 ∈ V
45 38 43 24 44 ovmpo ⊢ I ∈ ℕ ∧ J ∈ ℕ → I i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 J = if I < K I I + 1 if J < L J J + 1
46 21 45 syl ⊢ φ → I i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 J = if I < K I I + 1 if J < L J J + 1
47 9 10 opeq12d ⊢ φ → if I < K I I + 1 if J < L J J + 1 = X Y
48 46 47 eqtrd ⊢ φ → I i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 J = X Y
49 33 48 syl5eqr ⊢ φ → i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J = X Y
50 49 fveq2d ⊢ φ → A ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J = A ⁡ X Y
51 df-ov ⊢ X A Y = A ⁡ X Y
52 50 51 syl6eqr ⊢ φ → A ⁡ i ∈ ℕ , j ∈ ℕ ⟼ if i < K i i + 1 if j < L j j + 1 ⁡ I J = X A Y
53 32 52 eqtrd ⊢ φ → I S J = X A Y