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 ⊢ 𝑀 = ( litMat ‘ 𝑊 )
lmatfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lmatfval.w ⊢ ( 𝜑 → 𝑊 ∈ Word Word 𝑉 )
lmatfval.1 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑁 )
lmatfval.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 )
lmatfvlem.1 ⊢ 𝐾 ∈ ℕ0
lmatfvlem.2 ⊢ 𝐿 ∈ ℕ0
lmatfvlem.3 ⊢ 𝐼 ≤ 𝑁
lmatfvlem.4 ⊢ 𝐽 ≤ 𝑁
lmatfvlem.5 ⊢ ( 𝐾 + 1 ) = 𝐼
lmatfvlem.6 ⊢ ( 𝐿 + 1 ) = 𝐽
lmatfvlem.7 ⊢ ( 𝑊 ‘ 𝐾 ) = 𝑋
lmatfvlem.8 ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐿 ) = 𝑌 )
Assertion lmatfvlem ( 𝜑 → ( 𝐼 𝑀 𝐽 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 lmatfval.m ⊢ 𝑀 = ( litMat ‘ 𝑊 )
2 lmatfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lmatfval.w ⊢ ( 𝜑 → 𝑊 ∈ Word Word 𝑉 )
4 lmatfval.1 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑁 )
5 lmatfval.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 )
6 lmatfvlem.1 ⊢ 𝐾 ∈ ℕ0
7 lmatfvlem.2 ⊢ 𝐿 ∈ ℕ0
8 lmatfvlem.3 ⊢ 𝐼 ≤ 𝑁
9 lmatfvlem.4 ⊢ 𝐽 ≤ 𝑁
10 lmatfvlem.5 ⊢ ( 𝐾 + 1 ) = 𝐼
11 lmatfvlem.6 ⊢ ( 𝐿 + 1 ) = 𝐽
12 lmatfvlem.7 ⊢ ( 𝑊 ‘ 𝐾 ) = 𝑋
13 lmatfvlem.8 ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐿 ) = 𝑌 )
14 nn0p1nn ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ )
15 6 14 ax-mp ⊢ ( 𝐾 + 1 ) ∈ ℕ
16 10 15 eqeltrri ⊢ 𝐼 ∈ ℕ
17 nnge1 ⊢ ( 𝐼 ∈ ℕ → 1 ≤ 𝐼 )
18 16 17 ax-mp ⊢ 1 ≤ 𝐼
19 18 8 pm3.2i ⊢ ( 1 ≤ 𝐼 ∧ 𝐼 ≤ 𝑁 )
20 19 a1i ⊢ ( 𝜑 → ( 1 ≤ 𝐼 ∧ 𝐼 ≤ 𝑁 ) )
21 nnz ⊢ ( 𝐼 ∈ ℕ → 𝐼 ∈ ℤ )
22 16 21 ax-mp ⊢ 𝐼 ∈ ℤ
23 22 a1i ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
24 1z ⊢ 1 ∈ ℤ
25 24 a1i ⊢ ( 𝜑 → 1 ∈ ℤ )
26 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
27 elfz ⊢ ( ( 𝐼 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐼 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝐼 ∧ 𝐼 ≤ 𝑁 ) ) )
28 23 25 26 27 syl3anc ⊢ ( 𝜑 → ( 𝐼 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝐼 ∧ 𝐼 ≤ 𝑁 ) ) )
29 20 28 mpbird ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
30 nn0p1nn ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 + 1 ) ∈ ℕ )
31 7 30 ax-mp ⊢ ( 𝐿 + 1 ) ∈ ℕ
32 11 31 eqeltrri ⊢ 𝐽 ∈ ℕ
33 nnge1 ⊢ ( 𝐽 ∈ ℕ → 1 ≤ 𝐽 )
34 32 33 ax-mp ⊢ 1 ≤ 𝐽
35 34 9 pm3.2i ⊢ ( 1 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 )
36 35 a1i ⊢ ( 𝜑 → ( 1 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) )
37 nnz ⊢ ( 𝐽 ∈ ℕ → 𝐽 ∈ ℤ )
38 32 37 ax-mp ⊢ 𝐽 ∈ ℤ
39 38 a1i ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
40 elfz ⊢ ( ( 𝐽 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
41 39 25 26 40 syl3anc ⊢ ( 𝜑 → ( 𝐽 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
42 36 41 mpbird ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
43 1 2 3 4 5 29 42 lmatfval ⊢ ( 𝜑 → ( 𝐼 𝑀 𝐽 ) = ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) )
44 6 nn0cni ⊢ 𝐾 ∈ ℂ
45 ax-1cn ⊢ 1 ∈ ℂ
46 44 45 pncan3oi ⊢ ( ( 𝐾 + 1 ) − 1 ) = 𝐾
47 10 oveq1i ⊢ ( ( 𝐾 + 1 ) − 1 ) = ( 𝐼 − 1 )
48 46 47 eqtr3i ⊢ 𝐾 = ( 𝐼 − 1 )
49 48 fveq2i ⊢ ( 𝑊 ‘ 𝐾 ) = ( 𝑊 ‘ ( 𝐼 − 1 ) )
50 49 12 eqtr3i ⊢ ( 𝑊 ‘ ( 𝐼 − 1 ) ) = 𝑋
51 50 a1i ⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐼 − 1 ) ) = 𝑋 )
52 51 fveq1d ⊢ ( 𝜑 → ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) = ( 𝑋 ‘ ( 𝐽 − 1 ) ) )
53 7 nn0cni ⊢ 𝐿 ∈ ℂ
54 53 45 pncan3oi ⊢ ( ( 𝐿 + 1 ) − 1 ) = 𝐿
55 11 oveq1i ⊢ ( ( 𝐿 + 1 ) − 1 ) = ( 𝐽 − 1 )
56 54 55 eqtr3i ⊢ 𝐿 = ( 𝐽 − 1 )
57 56 a1i ⊢ ( 𝜑 → 𝐿 = ( 𝐽 − 1 ) )
58 57 fveq2d ⊢ ( 𝜑 → ( 𝑋 ‘ 𝐿 ) = ( 𝑋 ‘ ( 𝐽 − 1 ) ) )
59 58 13 eqtr3d ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐽 − 1 ) ) = 𝑌 )
60 43 52 59 3eqtrd ⊢ ( 𝜑 → ( 𝐼 𝑀 𝐽 ) = 𝑌 )