| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lmatfval.m | . . . 4
⊢ 𝑀 = (litMat‘𝑊) | 
| 2 |  | lmatfval.w | . . . . 5
⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) | 
| 3 |  | lmatval 33813 | . . . . 5
⊢ (𝑊 ∈ Word Word 𝑉 → (litMat‘𝑊) = (𝑘 ∈ (1...(♯‘𝑊)), 𝑗 ∈ (1...(♯‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) | 
| 4 | 2, 3 | syl 17 | . . . 4
⊢ (𝜑 → (litMat‘𝑊) = (𝑘 ∈ (1...(♯‘𝑊)), 𝑗 ∈ (1...(♯‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) | 
| 5 | 1, 4 | eqtrid 2788 | . . 3
⊢ (𝜑 → 𝑀 = (𝑘 ∈ (1...(♯‘𝑊)), 𝑗 ∈ (1...(♯‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) | 
| 6 |  | lmatfval.1 | . . . . 5
⊢ (𝜑 → (♯‘𝑊) = 𝑁) | 
| 7 | 6 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (1...(♯‘𝑊)) = (1...𝑁)) | 
| 8 |  | lmatfval.n | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 9 |  | lbfzo0 13740 | . . . . . . 7
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) | 
| 10 | 8, 9 | sylibr 234 | . . . . . 6
⊢ (𝜑 → 0 ∈ (0..^𝑁)) | 
| 11 |  | 0nn0 12543 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 12 | 11 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) | 
| 13 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → 𝑖 = 0) | 
| 14 | 13 | eleq1d 2825 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑖 ∈ (0..^𝑁) ↔ 0 ∈ (0..^𝑁))) | 
| 15 | 13 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑊‘𝑖) = (𝑊‘0)) | 
| 16 | 15 | fveqeq2d 6913 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((♯‘(𝑊‘𝑖)) = 𝑁 ↔ (♯‘(𝑊‘0)) = 𝑁)) | 
| 17 | 14, 16 | imbi12d 344 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑖 ∈ (0..^𝑁) → (♯‘(𝑊‘𝑖)) = 𝑁) ↔ (0 ∈ (0..^𝑁) → (♯‘(𝑊‘0)) = 𝑁))) | 
| 18 |  | lmatfval.2 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁) | 
| 19 | 18 | ex 412 | . . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (0..^𝑁) → (♯‘(𝑊‘𝑖)) = 𝑁)) | 
| 20 | 12, 17, 19 | vtocld 3560 | . . . . . 6
⊢ (𝜑 → (0 ∈ (0..^𝑁) → (♯‘(𝑊‘0)) = 𝑁)) | 
| 21 | 10, 20 | mpd 15 | . . . . 5
⊢ (𝜑 → (♯‘(𝑊‘0)) = 𝑁) | 
| 22 | 21 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (1...(♯‘(𝑊‘0))) = (1...𝑁)) | 
| 23 |  | eqidd 2737 | . . . 4
⊢ (𝜑 → ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)) = ((𝑊‘(𝑘 − 1))‘(𝑗 − 1))) | 
| 24 | 7, 22, 23 | mpoeq123dv 7509 | . . 3
⊢ (𝜑 → (𝑘 ∈ (1...(♯‘𝑊)), 𝑗 ∈ (1...(♯‘(𝑊‘0))) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1))) = (𝑘 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) | 
| 25 | 5, 24 | eqtrd 2776 | . 2
⊢ (𝜑 → 𝑀 = (𝑘 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)))) | 
| 26 |  | lmatcl.1 | . . 3
⊢ 𝑂 = ((1...𝑁) Mat 𝑅) | 
| 27 |  | lmatcl.b | . . 3
⊢ 𝑉 = (Base‘𝑅) | 
| 28 |  | lmatcl.2 | . . 3
⊢ 𝑃 = (Base‘𝑂) | 
| 29 |  | fzfid 14015 | . . 3
⊢ (𝜑 → (1...𝑁) ∈ Fin) | 
| 30 |  | lmatcl.r | . . 3
⊢ (𝜑 → 𝑅 ∈ 𝑋) | 
| 31 | 2 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑊 ∈ Word Word 𝑉) | 
| 32 |  | simp2 1137 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑘 ∈ (1...𝑁)) | 
| 33 |  | fz1fzo0m1 13751 | . . . . . . 7
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ (0..^𝑁)) | 
| 34 | 32, 33 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑘 − 1) ∈ (0..^𝑁)) | 
| 35 | 6 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (♯‘𝑊) = 𝑁) | 
| 36 | 35 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (0..^(♯‘𝑊)) = (0..^𝑁)) | 
| 37 | 34, 36 | eleqtrrd 2843 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑘 − 1) ∈ (0..^(♯‘𝑊))) | 
| 38 |  | wrdsymbcl 14566 | . . . . 5
⊢ ((𝑊 ∈ Word Word 𝑉 ∧ (𝑘 − 1) ∈ (0..^(♯‘𝑊))) → (𝑊‘(𝑘 − 1)) ∈ Word 𝑉) | 
| 39 | 31, 37, 38 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑊‘(𝑘 − 1)) ∈ Word 𝑉) | 
| 40 |  | simp3 1138 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁)) | 
| 41 |  | fz1fzo0m1 13751 | . . . . . 6
⊢ (𝑗 ∈ (1...𝑁) → (𝑗 − 1) ∈ (0..^𝑁)) | 
| 42 | 40, 41 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0..^𝑁)) | 
| 43 |  | ovexd 7467 | . . . . . . . . . 10
⊢ (𝜑 → (𝑘 − 1) ∈ V) | 
| 44 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → 𝑖 = (𝑘 − 1)) | 
| 45 |  | eqidd 2737 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (0..^𝑁) = (0..^𝑁)) | 
| 46 | 44, 45 | eleq12d 2834 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (𝑖 ∈ (0..^𝑁) ↔ (𝑘 − 1) ∈ (0..^𝑁))) | 
| 47 | 44 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → (𝑊‘𝑖) = (𝑊‘(𝑘 − 1))) | 
| 48 | 47 | fveqeq2d 6913 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → ((♯‘(𝑊‘𝑖)) = 𝑁 ↔ (♯‘(𝑊‘(𝑘 − 1))) = 𝑁)) | 
| 49 | 46, 48 | imbi12d 344 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 = (𝑘 − 1)) → ((𝑖 ∈ (0..^𝑁) → (♯‘(𝑊‘𝑖)) = 𝑁) ↔ ((𝑘 − 1) ∈ (0..^𝑁) → (♯‘(𝑊‘(𝑘 − 1))) = 𝑁))) | 
| 50 | 43, 49, 19 | vtocld 3560 | . . . . . . . . 9
⊢ (𝜑 → ((𝑘 − 1) ∈ (0..^𝑁) → (♯‘(𝑊‘(𝑘 − 1))) = 𝑁)) | 
| 51 | 50 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 − 1) ∈ (0..^𝑁)) → (♯‘(𝑊‘(𝑘 − 1))) = 𝑁) | 
| 52 | 33, 51 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (♯‘(𝑊‘(𝑘 − 1))) = 𝑁) | 
| 53 | 52 | 3adant3 1132 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (♯‘(𝑊‘(𝑘 − 1))) = 𝑁) | 
| 54 | 53 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (0..^(♯‘(𝑊‘(𝑘 − 1)))) = (0..^𝑁)) | 
| 55 | 42, 54 | eleqtrrd 2843 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0..^(♯‘(𝑊‘(𝑘 − 1))))) | 
| 56 |  | wrdsymbcl 14566 | . . . 4
⊢ (((𝑊‘(𝑘 − 1)) ∈ Word 𝑉 ∧ (𝑗 − 1) ∈ (0..^(♯‘(𝑊‘(𝑘 − 1))))) → ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)) ∈ 𝑉) | 
| 57 | 39, 55, 56 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑊‘(𝑘 − 1))‘(𝑗 − 1)) ∈ 𝑉) | 
| 58 | 26, 27, 28, 29, 30, 57 | matbas2d 22430 | . 2
⊢ (𝜑 → (𝑘 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑊‘(𝑘 − 1))‘(𝑗 − 1))) ∈ 𝑃) | 
| 59 | 25, 58 | eqeltrd 2840 | 1
⊢ (𝜑 → 𝑀 ∈ 𝑃) |