Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lmat Structured version   Visualization version   GIF version

Definition df-lmat 31065
Description: Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.)
Assertion
Ref Expression
df-lmat litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))
Distinct variable group:   𝑖,𝑗,𝑚

Detailed syntax breakdown of Definition df-lmat
StepHypRef Expression
1 clmat 31064 . 2 class litMat
2 vm . . 3 setvar 𝑚
3 cvv 3493 . . 3 class V
4 vi . . . 4 setvar 𝑖
5 vj . . . 4 setvar 𝑗
6 c1 10530 . . . . 5 class 1
72cv 1529 . . . . . 6 class 𝑚
8 chash 13682 . . . . . 6 class
97, 8cfv 6348 . . . . 5 class (♯‘𝑚)
10 cfz 12884 . . . . 5 class ...
116, 9, 10co 7148 . . . 4 class (1...(♯‘𝑚))
12 cc0 10529 . . . . . . 7 class 0
1312, 7cfv 6348 . . . . . 6 class (𝑚‘0)
1413, 8cfv 6348 . . . . 5 class (♯‘(𝑚‘0))
156, 14, 10co 7148 . . . 4 class (1...(♯‘(𝑚‘0)))
165cv 1529 . . . . . 6 class 𝑗
17 cmin 10862 . . . . . 6 class
1816, 6, 17co 7148 . . . . 5 class (𝑗 − 1)
194cv 1529 . . . . . . 7 class 𝑖
2019, 6, 17co 7148 . . . . . 6 class (𝑖 − 1)
2120, 7cfv 6348 . . . . 5 class (𝑚‘(𝑖 − 1))
2218, 21cfv 6348 . . . 4 class ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))
234, 5, 11, 15, 22cmpo 7150 . . 3 class (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1)))
242, 3, 23cmpt 5137 . 2 class (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))
251, 24wceq 1530 1 wff litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))
Colors of variables: wff setvar class
This definition is referenced by:  lmatval  31066
  Copyright terms: Public domain W3C validator