Step | Hyp | Ref
| Expression |
1 | | lmatfval.m |
. . 3
⊢ 𝑀 = (litMat‘𝑊) |
2 | | lmatfval.w |
. . . 4
⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) |
3 | | lmatval 29207 |
. . . 4
⊢ (𝑊 ∈ Word Word 𝑉 → (litMat‘𝑊) = (𝑖 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑖 − 1))‘(𝑗 − 1)))) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → (litMat‘𝑊) = (𝑖 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑖 − 1))‘(𝑗 − 1)))) |
5 | 1, 4 | syl5eq 2656 |
. 2
⊢ (𝜑 → 𝑀 = (𝑖 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑖 − 1))‘(𝑗 − 1)))) |
6 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → 𝑖 = 𝐼) |
7 | 6 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → (𝑖 − 1) = (𝐼 − 1)) |
8 | 7 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → (𝑊‘(𝑖 − 1)) = (𝑊‘(𝐼 − 1))) |
9 | | simprr 792 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → 𝑗 = 𝐽) |
10 | 9 | oveq1d 6564 |
. . 3
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → (𝑗 − 1) = (𝐽 − 1)) |
11 | 8, 10 | fveq12d 6109 |
. 2
⊢ ((𝜑 ∧ (𝑖 = 𝐼 ∧ 𝑗 = 𝐽)) → ((𝑊‘(𝑖 − 1))‘(𝑗 − 1)) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1))) |
12 | | lmatfval.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) |
13 | | lmatfval.1 |
. . . 4
⊢ (𝜑 → (#‘𝑊) = 𝑁) |
14 | 13 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (1...(#‘𝑊)) = (1...𝑁)) |
15 | 12, 14 | eleqtrrd 2691 |
. 2
⊢ (𝜑 → 𝐼 ∈ (1...(#‘𝑊))) |
16 | | lmatfval.j |
. . 3
⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) |
17 | | 1m1e0 10966 |
. . . . . 6
⊢ (1
− 1) = 0 |
18 | | lmatfval.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
19 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
20 | 18, 19 | syl6eleq 2698 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
21 | | eluzfz1 12219 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
22 | 20, 21 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 1 ∈ (1...𝑁)) |
23 | | fz1fzo0m1 12383 |
. . . . . . 7
⊢ (1 ∈
(1...𝑁) → (1 −
1) ∈ (0..^𝑁)) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1 − 1) ∈
(0..^𝑁)) |
25 | 17, 24 | syl5eqelr 2693 |
. . . . 5
⊢ (𝜑 → 0 ∈ (0..^𝑁)) |
26 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 = 0) |
27 | 26 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑖 ∈ (0..^𝑁) ↔ 0 ∈ (0..^𝑁))) |
28 | 26 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑊‘𝑖) = (𝑊‘0)) |
29 | 28 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → (#‘(𝑊‘𝑖)) = (#‘(𝑊‘0))) |
30 | 29 | eqeq1d 2612 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → ((#‘(𝑊‘𝑖)) = 𝑁 ↔ (#‘(𝑊‘0)) = 𝑁)) |
31 | 27, 30 | imbi12d 333 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 ∈ (0..^𝑁) → (#‘(𝑊‘𝑖)) = 𝑁) ↔ (0 ∈ (0..^𝑁) → (#‘(𝑊‘0)) = 𝑁))) |
32 | | lmatfval.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) |
33 | 32 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ (0..^𝑁) → (#‘(𝑊‘𝑖)) = 𝑁)) |
34 | 25, 31, 33 | vtocld 3230 |
. . . . 5
⊢ (𝜑 → (0 ∈ (0..^𝑁) → (#‘(𝑊‘0)) = 𝑁)) |
35 | 25, 34 | mpd 15 |
. . . 4
⊢ (𝜑 → (#‘(𝑊‘0)) = 𝑁) |
36 | 35 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (1...(#‘(𝑊‘0))) = (1...𝑁)) |
37 | 16, 36 | eleqtrrd 2691 |
. 2
⊢ (𝜑 → 𝐽 ∈ (1...(#‘(𝑊‘0)))) |
38 | | fz1fzo0m1 12383 |
. . . . . 6
⊢ (𝐼 ∈ (1...𝑁) → (𝐼 − 1) ∈ (0..^𝑁)) |
39 | 12, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 − 1) ∈ (0..^𝑁)) |
40 | 13 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (0..^(#‘𝑊)) = (0..^𝑁)) |
41 | 39, 40 | eleqtrrd 2691 |
. . . 4
⊢ (𝜑 → (𝐼 − 1) ∈ (0..^(#‘𝑊))) |
42 | | wrdsymbcl 13173 |
. . . 4
⊢ ((𝑊 ∈ Word Word 𝑉 ∧ (𝐼 − 1) ∈ (0..^(#‘𝑊))) → (𝑊‘(𝐼 − 1)) ∈ Word 𝑉) |
43 | 2, 41, 42 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑊‘(𝐼 − 1)) ∈ Word 𝑉) |
44 | | fz1fzo0m1 12383 |
. . . . 5
⊢ (𝐽 ∈ (1...𝑁) → (𝐽 − 1) ∈ (0..^𝑁)) |
45 | 16, 44 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐽 − 1) ∈ (0..^𝑁)) |
46 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = (𝐼 − 1)) → 𝑖 = (𝐼 − 1)) |
47 | 46 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = (𝐼 − 1)) → (𝑖 ∈ (0..^𝑁) ↔ (𝐼 − 1) ∈ (0..^𝑁))) |
48 | 46 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = (𝐼 − 1)) → (𝑊‘𝑖) = (𝑊‘(𝐼 − 1))) |
49 | 48 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = (𝐼 − 1)) → (#‘(𝑊‘𝑖)) = (#‘(𝑊‘(𝐼 − 1)))) |
50 | 49 | eqeq1d 2612 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = (𝐼 − 1)) → ((#‘(𝑊‘𝑖)) = 𝑁 ↔ (#‘(𝑊‘(𝐼 − 1))) = 𝑁)) |
51 | 47, 50 | imbi12d 333 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = (𝐼 − 1)) → ((𝑖 ∈ (0..^𝑁) → (#‘(𝑊‘𝑖)) = 𝑁) ↔ ((𝐼 − 1) ∈ (0..^𝑁) → (#‘(𝑊‘(𝐼 − 1))) = 𝑁))) |
52 | 39, 51, 33 | vtocld 3230 |
. . . . . 6
⊢ (𝜑 → ((𝐼 − 1) ∈ (0..^𝑁) → (#‘(𝑊‘(𝐼 − 1))) = 𝑁)) |
53 | 39, 52 | mpd 15 |
. . . . 5
⊢ (𝜑 → (#‘(𝑊‘(𝐼 − 1))) = 𝑁) |
54 | 53 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (0..^(#‘(𝑊‘(𝐼 − 1)))) = (0..^𝑁)) |
55 | 45, 54 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → (𝐽 − 1) ∈ (0..^(#‘(𝑊‘(𝐼 − 1))))) |
56 | | wrdsymbcl 13173 |
. . 3
⊢ (((𝑊‘(𝐼 − 1)) ∈ Word 𝑉 ∧ (𝐽 − 1) ∈ (0..^(#‘(𝑊‘(𝐼 − 1))))) → ((𝑊‘(𝐼 − 1))‘(𝐽 − 1)) ∈ 𝑉) |
57 | 43, 55, 56 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑊‘(𝐼 − 1))‘(𝐽 − 1)) ∈ 𝑉) |
58 | 5, 11, 15, 37, 57 | ovmpt2d 6686 |
1
⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1))) |