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 \in V ⟼ (i \in (1 \dots \|m\|), j \in (1 \dots \|m (0)\|) ⟼ m (i - 1) (j - 1)))$

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 \dots$
6		chash	$class \|.\|$
7	1	cv	$setvar m$
8	7 6	cfv	$class \|m\|$
9	4 8 5	co	$class (1 \dots \|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 \dots \|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 \in (1 \dots \|m\|), j \in (1 \dots \|m (0)\|) ⟼ m (i - 1) (j - 1))$
23	1 2 22	cmpt	$class (m \in V ⟼ (i \in (1 \dots \|m\|), j \in (1 \dots \|m (0)\|) ⟼ m (i - 1) (j - 1)))$
24	0 23	wceq	$wff litMat = (m \in V ⟼ (i \in (1 \dots \|m\|), j \in (1 \dots \|m (0)\|) ⟼ m (i - 1) (j - 1)))$

Metamath Proof Explorer