Theorem lmatfvlem

Description: Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020)

	Ref	Expression
Hypotheses	lmatfval.m	$$⊢M=\mathrm{litMat}\left(W\right)$$
	lmatfval.n	$$⊢\phi \to N\in \mathbb{N}$$
	lmatfval.w	$$⊢\phi \to W\in \mathrm{Word}\mathrm{Word}V$$
	lmatfval.1	$$⊢\phi \to \left|W\right|=N$$
	lmatfval.2	$$⊢\left(\phi \wedge i\in \left(0..^N\right)\right)\to \left|W\left(i\right)\right|=N$$
	lmatfvlem.1	$$⊢K\in {\mathbb{N}}_0$$
	lmatfvlem.2	$$⊢L\in {\mathbb{N}}_0$$
	lmatfvlem.3	$$⊢I\le N$$
	lmatfvlem.4	$$⊢J\le N$$
	lmatfvlem.5	$$⊢K+1=I$$
	lmatfvlem.6	$$⊢L+1=J$$
	lmatfvlem.7	$$⊢W\left(K\right)=X$$
	lmatfvlem.8	$$⊢\phi \to X\left(L\right)=Y$$
Assertion	lmatfvlem	$$⊢\phi \to IMJ=Y$$

Proof

Step	Hyp	Ref	Expression
1		lmatfval.m	$$⊢M=\mathrm{litMat}\left(W\right)$$
2		lmatfval.n	$$⊢\phi \to N\in \mathbb{N}$$
3		lmatfval.w	$$⊢\phi \to W\in \mathrm{Word}\mathrm{Word}V$$
4		lmatfval.1	$$⊢\phi \to \left|W\right|=N$$
5		lmatfval.2	$$⊢\left(\phi \wedge i\in \left(0..^N\right)\right)\to \left|W\left(i\right)\right|=N$$
6		lmatfvlem.1	$$⊢K\in {\mathbb{N}}_0$$
7		lmatfvlem.2	$$⊢L\in {\mathbb{N}}_0$$
8		lmatfvlem.3	$$⊢I\le N$$
9		lmatfvlem.4	$$⊢J\le N$$
10		lmatfvlem.5	$$⊢K+1=I$$
11		lmatfvlem.6	$$⊢L+1=J$$
12		lmatfvlem.7	$$⊢W\left(K\right)=X$$
13		lmatfvlem.8	$$⊢\phi \to X\left(L\right)=Y$$
14		nn0p1nn	$$⊢K\in {\mathbb{N}}_0\to K+1\in \mathbb{N}$$
15	6 14	ax-mp	$$⊢K+1\in \mathbb{N}$$
16	10 15	eqeltrri	$$⊢I\in \mathbb{N}$$
17		nnge1	$$⊢I\in \mathbb{N}\to 1\le I$$
18	16 17	ax-mp	$$⊢1\le I$$
19	18 8	pm3.2i	$$⊢\left(1\le I\wedge I\le N\right)$$
20	19	a1i	$$⊢\phi \to \left(1\le I\wedge I\le N\right)$$
21		nnz	$$⊢I\in \mathbb{N}\to I\in \mathbb{Z}$$
22	16 21	ax-mp	$$⊢I\in \mathbb{Z}$$
23	22	a1i	$$⊢\phi \to I\in \mathbb{Z}$$
24		1z	$$⊢1\in \mathbb{Z}$$
25	24	a1i	$$⊢\phi \to 1\in \mathbb{Z}$$
26	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
27		elfz	$$⊢\left(I\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(I\in \left(1\dots N\right)\leftrightarrow \left(1\le I\wedge I\le N\right)\right)$$
28	23 25 26 27	syl3anc	$$⊢\phi \to \left(I\in \left(1\dots N\right)\leftrightarrow \left(1\le I\wedge I\le N\right)\right)$$
29	20 28	mpbird	$$⊢\phi \to I\in \left(1\dots N\right)$$
30		nn0p1nn	$$⊢L\in {\mathbb{N}}_0\to L+1\in \mathbb{N}$$
31	7 30	ax-mp	$$⊢L+1\in \mathbb{N}$$
32	11 31	eqeltrri	$$⊢J\in \mathbb{N}$$
33		nnge1	$$⊢J\in \mathbb{N}\to 1\le J$$
34	32 33	ax-mp	$$⊢1\le J$$
35	34 9	pm3.2i	$$⊢\left(1\le J\wedge J\le N\right)$$
36	35	a1i	$$⊢\phi \to \left(1\le J\wedge J\le N\right)$$
37		nnz	$$⊢J\in \mathbb{N}\to J\in \mathbb{Z}$$
38	32 37	ax-mp	$$⊢J\in \mathbb{Z}$$
39	38	a1i	$$⊢\phi \to J\in \mathbb{Z}$$
40		elfz	$$⊢\left(J\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(J\in \left(1\dots N\right)\leftrightarrow \left(1\le J\wedge J\le N\right)\right)$$
41	39 25 26 40	syl3anc	$$⊢\phi \to \left(J\in \left(1\dots N\right)\leftrightarrow \left(1\le J\wedge J\le N\right)\right)$$
42	36 41	mpbird	$$⊢\phi \to J\in \left(1\dots N\right)$$
43	1 2 3 4 5 29 42	lmatfval	$$⊢\phi \to IMJ=W\left(I-1\right)\left(J-1\right)$$
44	6	nn0cni	$$⊢K\in ℂ$$
45		ax-1cn	$$⊢1\in ℂ$$
46	44 45	pncan3oi	$$⊢K+1-1=K$$
47	10	oveq1i	$$⊢K+1-1=I-1$$
48	46 47	eqtr3i	$$⊢K=I-1$$
49	48	fveq2i	$$⊢W\left(K\right)=W\left(I-1\right)$$
50	49 12	eqtr3i	$$⊢W\left(I-1\right)=X$$
51	50	a1i	$$⊢\phi \to W\left(I-1\right)=X$$
52	51	fveq1d	$$⊢\phi \to W\left(I-1\right)\left(J-1\right)=X\left(J-1\right)$$
53	7	nn0cni	$$⊢L\in ℂ$$
54	53 45	pncan3oi	$$⊢L+1-1=L$$
55	11	oveq1i	$$⊢L+1-1=J-1$$
56	54 55	eqtr3i	$$⊢L=J-1$$
57	56	a1i	$$⊢\phi \to L=J-1$$
58	57	fveq2d	$$⊢\phi \to X\left(L\right)=X\left(J-1\right)$$
59	58 13	eqtr3d	$$⊢\phi \to X\left(J-1\right)=Y$$
60	43 52 59	3eqtrd	$$⊢\phi \to IMJ=Y$$