Definition df-lmat

Description: Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020)

	Ref	Expression
Assertion	df-lmat	⊢ litMat = ( 𝑚 ∈ V ↦ ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑚 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) ↦ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmat	⊢ litMat
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vi	⊢ 𝑖
4		c1	⊢ 1
5		cfz	⊢ ...
6		chash	⊢ ♯
7	1	cv	⊢ 𝑚
8	7 6	cfv	⊢ ( ♯ ‘ 𝑚 )
9	4 8 5	co	⊢ ( 1 ... ( ♯ ‘ 𝑚 ) )
10		vj	⊢ 𝑗
11		cc0	⊢ 0
12	11 7	cfv	⊢ ( 𝑚 ‘ 0 )
13	12 6	cfv	⊢ ( ♯ ‘ ( 𝑚 ‘ 0 ) )
14	4 13 5	co	⊢ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) )
15	3	cv	⊢ 𝑖
16		cmin	⊢ −
17	15 4 16	co	⊢ ( 𝑖 − 1 )
18	17 7	cfv	⊢ ( 𝑚 ‘ ( 𝑖 − 1 ) )
19	10	cv	⊢ 𝑗
20	19 4 16	co	⊢ ( 𝑗 − 1 )
21	20 18	cfv	⊢ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) )
22	3 10 9 14 21	cmpo	⊢ ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑚 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) ↦ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) )
23	1 2 22	cmpt	⊢ ( 𝑚 ∈ V ↦ ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑚 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) ↦ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
24	0 23	wceq	⊢ litMat = ( 𝑚 ∈ V ↦ ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑚 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑚 ‘ 0 ) ) ) ↦ ( ( 𝑚 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )