Step | Hyp | Ref
| Expression |
1 | | lmatfval.m |
. . . 4
⊢ 𝑀 = (litMat‘𝑊) |
2 | | lmatfval.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) |
3 | | lmatval 29879 |
. . . . 5
⊢ (𝑊 ∈ Word Word 𝑉 → (litMat‘𝑊) = (𝑘 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) |
4 | 2, 3 | syl 17 |
. . . 4
⊢ (𝜑 → (litMat‘𝑊) = (𝑘 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) |
5 | 1, 4 | syl5eq 2668 |
. . 3
⊢ (𝜑 → 𝑀 = (𝑘 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) |
6 | | lmatfval.1 |
. . . . 5
⊢ (𝜑 → (#‘𝑊) = 𝑁) |
7 | 6 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (1...(#‘𝑊)) = (1...𝑁)) |
8 | | lmatfval.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | | lbfzo0 12507 |
. . . . . . 7
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
10 | 8, 9 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0..^𝑁)) |
11 | | 0nn0 11307 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) |
13 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 = 0) |
14 | 13 | eleq1d 2686 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑖 ∈ (0..^𝑁) ↔ 0 ∈ (0..^𝑁))) |
15 | 13 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑊‘𝑖) = (𝑊‘0)) |
16 | 15 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (#‘(𝑊‘𝑖)) = (#‘(𝑊‘0))) |
17 | 16 | eqeq1d 2624 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((#‘(𝑊‘𝑖)) = 𝑁 ↔ (#‘(𝑊‘0)) = 𝑁)) |
18 | 14, 17 | imbi12d 334 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 ∈ (0..^𝑁) → (#‘(𝑊‘𝑖)) = 𝑁) ↔ (0 ∈ (0..^𝑁) → (#‘(𝑊‘0)) = 𝑁))) |
19 | | lmatfval.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (#‘(𝑊‘𝑖)) = 𝑁) |
20 | 19 | ex 450 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (0..^𝑁) → (#‘(𝑊‘𝑖)) = 𝑁)) |
21 | 12, 18, 20 | vtocld 3257 |
. . . . . 6
⊢ (𝜑 → (0 ∈ (0..^𝑁) → (#‘(𝑊‘0)) = 𝑁)) |
22 | 10, 21 | mpd 15 |
. . . . 5
⊢ (𝜑 → (#‘(𝑊‘0)) = 𝑁) |
23 | 22 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (1...(#‘(𝑊‘0))) = (1...𝑁)) |
24 | | eqidd 2623 |
. . . 4
⊢ (𝜑 → ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)) = ((𝑊‘(𝑘 − 1))‘(𝑗 − 1))) |
25 | 7, 23, 24 | mpt2eq123dv 6717 |
. . 3
⊢ (𝜑 → (𝑘 ∈ (1...(#‘𝑊)), 𝑗 ∈ (1...(#‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1))) = (𝑘 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) |
26 | 5, 25 | eqtrd 2656 |
. 2
⊢ (𝜑 → 𝑀 = (𝑘 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) |
27 | | lmatcl.1 |
. . 3
⊢ 𝑂 = ((1...𝑁) Mat 𝑅) |
28 | | lmatcl.b |
. . 3
⊢ 𝑉 = (Base‘𝑅) |
29 | | lmatcl.2 |
. . 3
⊢ 𝑃 = (Base‘𝑂) |
30 | | fzfid 12772 |
. . 3
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
31 | | lmatcl.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ 𝑋) |
32 | 2 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑊 ∈ Word Word 𝑉) |
33 | | simp2 1062 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑘 ∈ (1...𝑁)) |
34 | | fz1fzo0m1 12515 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ (0..^𝑁)) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑘 − 1) ∈ (0..^𝑁)) |
36 | 6 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (#‘𝑊) = 𝑁) |
37 | 36 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (0..^(#‘𝑊)) = (0..^𝑁)) |
38 | 35, 37 | eleqtrrd 2704 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑘 − 1) ∈ (0..^(#‘𝑊))) |
39 | | wrdsymbcl 13318 |
. . . . 5
⊢ ((𝑊 ∈ Word Word 𝑉 ∧ (𝑘 − 1) ∈ (0..^(#‘𝑊))) → (𝑊‘(𝑘 − 1)) ∈ Word 𝑉) |
40 | 32, 38, 39 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑊‘(𝑘 − 1)) ∈ Word 𝑉) |
41 | | simp3 1063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) |
42 | | fz1fzo0m1 12515 |
. . . . . 6
⊢ (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0..^𝑁)) |
43 | 41, 42 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0..^𝑁)) |
44 | | ovexd 6680 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 − 1) ∈ V) |
45 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → 𝑖 = (𝑘 − 1)) |
46 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (0..^𝑁) = (0..^𝑁)) |
47 | 45, 46 | eleq12d 2695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (𝑖 ∈ (0..^𝑁) ↔ (𝑘 − 1) ∈ (0..^𝑁))) |
48 | 45 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (𝑊‘𝑖) = (𝑊‘(𝑘 − 1))) |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (#‘(𝑊‘𝑖)) = (#‘(𝑊‘(𝑘 − 1)))) |
50 | 49 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → ((#‘(𝑊‘𝑖)) = 𝑁 ↔ (#‘(𝑊‘(𝑘 − 1))) = 𝑁)) |
51 | 47, 50 | imbi12d 334 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → ((𝑖 ∈ (0..^𝑁) → (#‘(𝑊‘𝑖)) = 𝑁) ↔ ((𝑘 − 1) ∈ (0..^𝑁) → (#‘(𝑊‘(𝑘 − 1))) = 𝑁))) |
52 | 44, 51, 20 | vtocld 3257 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑘 − 1) ∈ (0..^𝑁) → (#‘(𝑊‘(𝑘 − 1))) = 𝑁)) |
53 | 52 | imp 445 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 − 1) ∈ (0..^𝑁)) → (#‘(𝑊‘(𝑘 − 1))) = 𝑁) |
54 | 34, 53 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (#‘(𝑊‘(𝑘 − 1))) = 𝑁) |
55 | 54 | 3adant3 1081 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (#‘(𝑊‘(𝑘 − 1))) = 𝑁) |
56 | 55 | oveq2d 6666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (0..^(#‘(𝑊‘(𝑘 − 1)))) = (0..^𝑁)) |
57 | 43, 56 | eleqtrrd 2704 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0..^(#‘(𝑊‘(𝑘 − 1))))) |
58 | | wrdsymbcl 13318 |
. . . 4
⊢ (((𝑊‘(𝑘 − 1)) ∈ Word 𝑉 ∧ (𝑗 − 1) ∈ (0..^(#‘(𝑊‘(𝑘 − 1))))) → ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)) ∈ 𝑉) |
59 | 40, 57, 58 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)) ∈ 𝑉) |
60 | 27, 28, 29, 30, 31, 59 | matbas2d 20229 |
. 2
⊢ (𝜑 → (𝑘 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1))) ∈ 𝑃) |
61 | 26, 60 | eqeltrd 2701 |
1
⊢ (𝜑 → 𝑀 ∈ 𝑃) |