lmatfval

Description: Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020)

	Ref	Expression
Hypotheses	lmatfval.m	$⊢ M = litMat (W)$
	lmatfval.n	$⊢ φ \to N \in ℕ$
	lmatfval.w	$⊢ φ \to W \in Word Word V$
	lmatfval.1	$⊢ φ \to \|W\| = N$
	lmatfval.2	$⊢ (φ \land i \in (0 ..^N)) \to \|W (i)\| = N$
	lmatfval.i	$⊢ φ \to I \in (1 \dots N)$
	lmatfval.j	$⊢ φ \to J \in (1 \dots N)$
Assertion	lmatfval	$⊢ φ \to I M J = W (I - 1) (J - 1)$

Proof

Step	Hyp	Ref	Expression
1		lmatfval.m	$⊢ M = litMat (W)$
2		lmatfval.n	$⊢ φ \to N \in ℕ$
3		lmatfval.w	$⊢ φ \to W \in Word Word V$
4		lmatfval.1	$⊢ φ \to \|W\| = N$
5		lmatfval.2	$⊢ (φ \land i \in (0 ..^N)) \to \|W (i)\| = N$
6		lmatfval.i	$⊢ φ \to I \in (1 \dots N)$
7		lmatfval.j	$⊢ φ \to J \in (1 \dots N)$
8		lmatval	$⊢ W \in Word Word V \to litMat (W) = (i \in (1 \dots \|W\|), j \in (1 \dots \|W (0)\|) ⟼ W (i - 1) (j - 1))$
9	3 8	syl	$⊢ φ \to litMat (W) = (i \in (1 \dots \|W\|), j \in (1 \dots \|W (0)\|) ⟼ W (i - 1) (j - 1))$
10	1 9	eqtrid	$⊢ φ \to M = (i \in (1 \dots \|W\|), j \in (1 \dots \|W (0)\|) ⟼ W (i - 1) (j - 1))$
11		simprl	$⊢ (φ \land (i = I \land j = J)) \to i = I$
12	11	fvoveq1d	$⊢ (φ \land (i = I \land j = J)) \to W (i - 1) = W (I - 1)$
13		simprr	$⊢ (φ \land (i = I \land j = J)) \to j = J$
14	13	oveq1d	$⊢ (φ \land (i = I \land j = J)) \to j - 1 = J - 1$
15	12 14	fveq12d	$⊢ (φ \land (i = I \land j = J)) \to W (i - 1) (j - 1) = W (I - 1) (J - 1)$
16	4	oveq2d	$⊢ φ \to (1 \dots \|W\|) = (1 \dots N)$
17	6 16	eleqtrrd	$⊢ φ \to I \in (1 \dots \|W\|)$
18		1m1e0	$⊢ 1 - 1 = 0$
19		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
20	2 19	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 1}$
21		eluzfz1	$⊢ N \in ℤ_{\geq 1} \to 1 \in (1 \dots N)$
22	20 21	syl	$⊢ φ \to 1 \in (1 \dots N)$
23		fz1fzo0m1	$⊢ 1 \in (1 \dots N) \to 1 - 1 \in (0 ..^N)$
24	22 23	syl	$⊢ φ \to 1 - 1 \in (0 ..^N)$
25	18 24	eqeltrrid	$⊢ φ \to 0 \in (0 ..^N)$
26		simpr	$⊢ (φ \land i = 0) \to i = 0$
27	26	eleq1d	$⊢ (φ \land i = 0) \to (i \in (0 ..^N) \leftrightarrow 0 \in (0 ..^N))$
28	26	fveq2d	$⊢ (φ \land i = 0) \to W (i) = W (0)$
29	28	fveqeq2d	$⊢ (φ \land i = 0) \to (\|W (i)\| = N \leftrightarrow \|W (0)\| = N)$
30	27 29	imbi12d	$⊢ (φ \land i = 0) \to ((i \in (0 ..^N) \to \|W (i)\| = N) \leftrightarrow (0 \in (0 ..^N) \to \|W (0)\| = N))$
31	5	ex	$⊢ φ \to (i \in (0 ..^N) \to \|W (i)\| = N)$
32	25 30 31	vtocld	$⊢ φ \to (0 \in (0 ..^N) \to \|W (0)\| = N)$
33	25 32	mpd	$⊢ φ \to \|W (0)\| = N$
34	33	oveq2d	$⊢ φ \to (1 \dots \|W (0)\|) = (1 \dots N)$
35	7 34	eleqtrrd	$⊢ φ \to J \in (1 \dots \|W (0)\|)$
36		fz1fzo0m1	$⊢ I \in (1 \dots N) \to I - 1 \in (0 ..^N)$
37	6 36	syl	$⊢ φ \to I - 1 \in (0 ..^N)$
38	4	oveq2d	$⊢ φ \to (0 ..^\|W\|) = (0 ..^N)$
39	37 38	eleqtrrd	$⊢ φ \to I - 1 \in (0 ..^\|W\|)$
40		wrdsymbcl	$⊢ (W \in Word Word V \land I - 1 \in (0 ..^\|W\|)) \to W (I - 1) \in Word V$
41	3 39 40	syl2anc	$⊢ φ \to W (I - 1) \in Word V$
42		fz1fzo0m1	$⊢ J \in (1 \dots N) \to J - 1 \in (0 ..^N)$
43	7 42	syl	$⊢ φ \to J - 1 \in (0 ..^N)$
44		simpr	$⊢ (φ \land i = I - 1) \to i = I - 1$
45	44	eleq1d	$⊢ (φ \land i = I - 1) \to (i \in (0 ..^N) \leftrightarrow I - 1 \in (0 ..^N))$
46	44	fveq2d	$⊢ (φ \land i = I - 1) \to W (i) = W (I - 1)$
47	46	fveqeq2d	$⊢ (φ \land i = I - 1) \to (\|W (i)\| = N \leftrightarrow \|W (I - 1)\| = N)$
48	45 47	imbi12d	$⊢ (φ \land i = I - 1) \to ((i \in (0 ..^N) \to \|W (i)\| = N) \leftrightarrow (I - 1 \in (0 ..^N) \to \|W (I - 1)\| = N))$
49	37 48 31	vtocld	$⊢ φ \to (I - 1 \in (0 ..^N) \to \|W (I - 1)\| = N)$
50	37 49	mpd	$⊢ φ \to \|W (I - 1)\| = N$
51	50	oveq2d	$⊢ φ \to (0 ..^\|W (I - 1)\|) = (0 ..^N)$
52	43 51	eleqtrrd	$⊢ φ \to J - 1 \in (0 ..^\|W (I - 1)\|)$
53		wrdsymbcl	$⊢ (W (I - 1) \in Word V \land J - 1 \in (0 ..^\|W (I - 1)\|)) \to W (I - 1) (J - 1) \in V$
54	41 52 53	syl2anc	$⊢ φ \to W (I - 1) (J - 1) \in V$
55	10 15 17 35 54	ovmpod	$⊢ φ \to I M J = W (I - 1) (J - 1)$

Metamath Proof Explorer

Theorem lmatfval

Proof