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 e. _V |-> ( i e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmat 
 |-  litMat
1 vm 
 |-  m
2 cvv 
 |-  _V
3 vi 
 |-  i
4 c1 
 |-  1
5 cfz 
 |-  ...
6 chash 
 |-  #
7 1 cv 
 |-  m
8 7 6 cfv 
 |-  ( # ` m )
9 4 8 5 co 
 |-  ( 1 ... ( # ` m ) )
10 vj 
 |-  j
11 cc0 
 |-  0
12 11 7 cfv 
 |-  ( m ` 0 )
13 12 6 cfv 
 |-  ( # ` ( m ` 0 ) )
14 4 13 5 co 
 |-  ( 1 ... ( # ` ( m ` 0 ) ) )
15 3 cv 
 |-  i
16 cmin 
 |-  -
17 15 4 16 co 
 |-  ( i - 1 )
18 17 7 cfv 
 |-  ( m ` ( i - 1 ) )
19 10 cv 
 |-  j
20 19 4 16 co 
 |-  ( j - 1 )
21 20 18 cfv 
 |-  ( ( m ` ( i - 1 ) ) ` ( j - 1 ) )
22 3 10 9 14 21 cmpo 
 |-  ( i e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) )
23 1 2 22 cmpt 
 |-  ( m e. _V |-> ( i e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
24 0 23 wceq 
 |-  litMat = ( m e. _V |-> ( i e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) ) )