Definition df-lmat 33811

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 33810	. 2 class litMat
2		vm	. . 3 setvar 𝑚
3		cvv 3480	. . 3 class V
4		vi	. . . 4 setvar 𝑖
5		vj	. . . 4 setvar 𝑗
6		c1 11156	. . . . 5 class 1
7	2	cv 1539	. . . . . 6 class 𝑚
8		chash 14369	. . . . . 6 class ♯
9	7, 8	cfv 6561	. . . . 5 class (♯‘𝑚)
10		cfz 13547	. . . . 5 class ...
11	6, 9, 10	co 7431	. . . 4 class (1...(♯‘𝑚))
12		cc0 11155	. . . . . . 7 class 0
13	12, 7	cfv 6561	. . . . . 6 class (𝑚‘0)
14	13, 8	cfv 6561	. . . . 5 class (♯‘(𝑚‘0))
15	6, 14, 10	co 7431	. . . 4 class (1...(♯‘(𝑚‘0)))
16	5	cv 1539	. . . . . 6 class 𝑗
17		cmin 11492	. . . . . 6 class −
18	16, 6, 17	co 7431	. . . . 5 class (𝑗 − 1)
19	4	cv 1539	. . . . . . 7 class 𝑖
20	19, 6, 17	co 7431	. . . . . 6 class (𝑖 − 1)
21	20, 7	cfv 6561	. . . . 5 class (𝑚‘(𝑖 − 1))
22	18, 21	cfv 6561	. . . 4 class ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))
23	4, 5, 11, 15, 22	cmpo 7433	. . 3 class (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1)))
24	2, 3, 23	cmpt 5225	. 2 class (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))
25	1, 24	wceq 1540	1 wff litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1))))

This definition is referenced by:  lmatval  33812