Metamath Proof Explorer

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 = m ∈ V ⟼ i ∈ 1 … m , j ∈ 1 … m ⁡ 0 ⟼ m ⁡ i − 1 ⁡ j − 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmat class litMat
1 vm setvar m
2 cvv class V
3 vi setvar i
4 c1 class 1
5 cfz class …
6 chash class .
7 1 cv setvar m
8 7 6 cfv class m
9 4 8 5 co class 1 … m
10 vj setvar j
11 cc0 class 0
12 11 7 cfv class m ⁡ 0
13 12 6 cfv class m ⁡ 0
14 4 13 5 co class 1 … m ⁡ 0
15 3 cv setvar i
16 cmin class −
17 15 4 16 co class i − 1
18 17 7 cfv class m ⁡ i − 1
19 10 cv setvar j
20 19 4 16 co class j − 1
21 20 18 cfv class m ⁡ i − 1 ⁡ j − 1
22 3 10 9 14 21 cmpo class i ∈ 1 … m , j ∈ 1 … m ⁡ 0 ⟼ m ⁡ i − 1 ⁡ j − 1
23 1 2 22 cmpt class m ∈ V ⟼ i ∈ 1 … m , j ∈ 1 … m ⁡ 0 ⟼ m ⁡ i − 1 ⁡ j − 1
24 0 23 wceq wff litMat = m ∈ V ⟼ i ∈ 1 … m , j ∈ 1 … m ⁡ 0 ⟼ m ⁡ i − 1 ⁡ j − 1