# Metamath Proof Explorer

## 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 ℕ$
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 {ℕ}_{0}$
lmatfvlem.2 ${⊢}{L}\in {ℕ}_{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 {I}{M}{J}={Y}$

### Proof

Step Hyp Ref Expression
1 lmatfval.m ${⊢}{M}=\mathrm{litMat}\left({W}\right)$
2 lmatfval.n ${⊢}{\phi }\to {N}\in ℕ$
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 {ℕ}_{0}$
7 lmatfvlem.2 ${⊢}{L}\in {ℕ}_{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 {ℕ}_{0}\to {K}+1\in ℕ$
15 6 14 ax-mp ${⊢}{K}+1\in ℕ$
16 10 15 eqeltrri ${⊢}{I}\in ℕ$
17 nnge1 ${⊢}{I}\in ℕ\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 ℕ\to {I}\in ℤ$
22 16 21 ax-mp ${⊢}{I}\in ℤ$
23 22 a1i ${⊢}{\phi }\to {I}\in ℤ$
24 1z ${⊢}1\in ℤ$
25 24 a1i ${⊢}{\phi }\to 1\in ℤ$
26 2 nnzd ${⊢}{\phi }\to {N}\in ℤ$
27 elfz ${⊢}\left({I}\in ℤ\wedge 1\in ℤ\wedge {N}\in ℤ\right)\to \left({I}\in \left(1\dots {N}\right)↔\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)↔\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 {ℕ}_{0}\to {L}+1\in ℕ$
31 7 30 ax-mp ${⊢}{L}+1\in ℕ$
32 11 31 eqeltrri ${⊢}{J}\in ℕ$
33 nnge1 ${⊢}{J}\in ℕ\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 ℕ\to {J}\in ℤ$
38 32 37 ax-mp ${⊢}{J}\in ℤ$
39 38 a1i ${⊢}{\phi }\to {J}\in ℤ$
40 elfz ${⊢}\left({J}\in ℤ\wedge 1\in ℤ\wedge {N}\in ℤ\right)\to \left({J}\in \left(1\dots {N}\right)↔\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)↔\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 {I}{M}{J}={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 {I}{M}{J}={Y}$