Definition df-lmat 29206

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

Step	Hyp	Ref	Expression
1		clmat 29205	. 2 class litMat
2		vm	. . 3 setvar 𝑚
3		cvv 3173	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5		vj	. . . 4 setvar 𝑗
6		c1 9816	. . . . 5 class 1
7	2	cv 1474	. . . . . 6 class 𝑚
8		chash 12979	. . . . . 6 class #
9	7, 8	cfv 5804	. . . . 5 class (#‘𝑚)
10		cfz 12197	. . . . 5 class ...
11	6, 9, 10	co 6549	. . . 4 class (1...(#‘𝑚))
12		cc0 9815	. . . . . . 7 class 0
13	12, 7	cfv 5804	. . . . . 6 class (𝑚‘0)
14	13, 8	cfv 5804	. . . . 5 class (#‘(𝑚‘0))
15	6, 14, 10	co 6549	. . . 4 class (1...(#‘(𝑚‘0)))
16	5	cv 1474	. . . . . 6 class 𝑗
17		cmin 10145	. . . . . 6 class −
18	16, 6, 17	co 6549	. . . . 5 class (𝑗 − 1)
19	4	cv 1474	. . . . . . 7 class 𝑖
20	19, 6, 17	co 6549	. . . . . 6 class (𝑖 − 1)
21	20, 7	cfv 5804	. . . . 5 class (𝑚‘(𝑖 − 1))
22	18, 21	cfv 5804	. . . 4 class ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))
23	4, 5, 11, 15, 22	cmpt2 6551	. . 3 class (𝑖 ∈ (1...(#‘𝑚)), 𝑗 ∈ (1...(#‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1)))
24	2, 3, 23	cmpt 4643	. 2 class (𝑚 ∈ V ↦ (𝑖 ∈ (1...(#‘𝑚)), 𝑗 ∈ (1...(#‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))
25	1, 24	wceq 1475	1 wff litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(#‘𝑚)), 𝑗 ∈ (1...(#‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))

This definition is referenced by:  lmatval  29207