Step | Hyp | Ref
| Expression |
1 | | smat.s |
. . . . . 6
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) |
2 | | fz1ssnn 13478 |
. . . . . . . 8
⊢
(1...𝑀) ⊆
ℕ |
3 | | smat.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) |
4 | 2, 3 | sselid 3943 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
5 | | fz1ssnn 13478 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
6 | | smat.l |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) |
7 | 5, 6 | sselid 3943 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ ℕ) |
8 | | smat.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) |
9 | | smatfval 32433 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) → (𝐾(subMat1‘𝐴)𝐿) = (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))) |
10 | 4, 7, 8, 9 | syl3anc 1372 |
. . . . . 6
⊢ (𝜑 → (𝐾(subMat1‘𝐴)𝐿) = (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))) |
11 | 1, 10 | eqtrid 2785 |
. . . . 5
⊢ (𝜑 → 𝑆 = (𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))) |
12 | 11 | oveqd 7375 |
. . . 4
⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼(𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))𝐽)) |
13 | | df-ov 7361 |
. . . 4
⊢ (𝐼(𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))𝐽) = ((𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))‘⟨𝐼, 𝐽⟩) |
14 | 12, 13 | eqtrdi 2789 |
. . 3
⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))‘⟨𝐼, 𝐽⟩)) |
15 | | smatlem.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℕ) |
16 | | smatlem.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℕ) |
17 | 15, 16 | jca 513 |
. . . . . 6
⊢ (𝜑 → (𝐼 ∈ ℕ ∧ 𝐽 ∈ ℕ)) |
18 | | opelxp 5670 |
. . . . . 6
⊢
(⟨𝐼, 𝐽⟩ ∈ (ℕ ×
ℕ) ↔ (𝐼 ∈
ℕ ∧ 𝐽 ∈
ℕ)) |
19 | 17, 18 | sylibr 233 |
. . . . 5
⊢ (𝜑 → ⟨𝐼, 𝐽⟩ ∈ (ℕ ×
ℕ)) |
20 | | eqid 2733 |
. . . . . 6
⊢ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) = (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) |
21 | | opex 5422 |
. . . . . 6
⊢
⟨if(𝑖 <
𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩ ∈ V |
22 | 20, 21 | dmmpo 8004 |
. . . . 5
⊢ dom
(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) = (ℕ ×
ℕ) |
23 | 19, 22 | eleqtrrdi 2845 |
. . . 4
⊢ (𝜑 → ⟨𝐼, 𝐽⟩ ∈ dom (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)) |
24 | 20 | mpofun 7481 |
. . . . 5
⊢ Fun
(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) |
25 | | fvco 6940 |
. . . . 5
⊢ ((Fun
(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) ∧ ⟨𝐼, 𝐽⟩ ∈ dom (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)) → ((𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))‘⟨𝐼, 𝐽⟩) = (𝐴‘((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩))) |
26 | 24, 25 | mpan 689 |
. . . 4
⊢
(⟨𝐼, 𝐽⟩ ∈ dom (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦
⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) → ((𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))‘⟨𝐼, 𝐽⟩) = (𝐴‘((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩))) |
27 | 23, 26 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))‘⟨𝐼, 𝐽⟩) = (𝐴‘((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩))) |
28 | 14, 27 | eqtrd 2773 |
. 2
⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐴‘((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩))) |
29 | | df-ov 7361 |
. . . . 5
⊢ (𝐼(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)𝐽) = ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩) |
30 | | breq1 5109 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → (𝑖 < 𝐾 ↔ 𝐼 < 𝐾)) |
31 | | id 22 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → 𝑖 = 𝐼) |
32 | | oveq1 7365 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1)) |
33 | 30, 31, 32 | ifbieq12d 4515 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)) = if(𝐼 < 𝐾, 𝐼, (𝐼 + 1))) |
34 | 33 | opeq1d 4837 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩ = ⟨if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩) |
35 | | breq1 5109 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → (𝑗 < 𝐿 ↔ 𝐽 < 𝐿)) |
36 | | id 22 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → 𝑗 = 𝐽) |
37 | | oveq1 7365 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐽 → (𝑗 + 1) = (𝐽 + 1)) |
38 | 35, 36, 37 | ifbieq12d 4515 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → if(𝑗 < 𝐿, 𝑗, (𝑗 + 1)) = if(𝐽 < 𝐿, 𝐽, (𝐽 + 1))) |
39 | 38 | opeq2d 4838 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ⟨if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩ = ⟨if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)), if(𝐽 < 𝐿, 𝐽, (𝐽 + 1))⟩) |
40 | | opex 5422 |
. . . . . . . 8
⊢
⟨if(𝐼 <
𝐾, 𝐼, (𝐼 + 1)), if(𝐽 < 𝐿, 𝐽, (𝐽 + 1))⟩ ∈ V |
41 | 34, 39, 20, 40 | ovmpo 7516 |
. . . . . . 7
⊢ ((𝐼 ∈ ℕ ∧ 𝐽 ∈ ℕ) → (𝐼(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)𝐽) = ⟨if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)), if(𝐽 < 𝐿, 𝐽, (𝐽 + 1))⟩) |
42 | 17, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐼(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)𝐽) = ⟨if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)), if(𝐽 < 𝐿, 𝐽, (𝐽 + 1))⟩) |
43 | | smatlem.1 |
. . . . . . 7
⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋) |
44 | | smatlem.2 |
. . . . . . 7
⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌) |
45 | 43, 44 | opeq12d 4839 |
. . . . . 6
⊢ (𝜑 → ⟨if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)), if(𝐽 < 𝐿, 𝐽, (𝐽 + 1))⟩ = ⟨𝑋, 𝑌⟩) |
46 | 42, 45 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → (𝐼(𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)𝐽) = ⟨𝑋, 𝑌⟩) |
47 | 29, 46 | eqtr3id 2787 |
. . . 4
⊢ (𝜑 → ((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩) = ⟨𝑋, 𝑌⟩) |
48 | 47 | fveq2d 6847 |
. . 3
⊢ (𝜑 → (𝐴‘((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩)) = (𝐴‘⟨𝑋, 𝑌⟩)) |
49 | | df-ov 7361 |
. . 3
⊢ (𝑋𝐴𝑌) = (𝐴‘⟨𝑋, 𝑌⟩) |
50 | 48, 49 | eqtr4di 2791 |
. 2
⊢ (𝜑 → (𝐴‘((𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩)‘⟨𝐼, 𝐽⟩)) = (𝑋𝐴𝑌)) |
51 | 28, 50 | eqtrd 2773 |
1
⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌)) |