Metamath Proof Explorer

Theorem lmatfval

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

Ref Expression
Hypotheses lmatfval.m ⊢ 𝑀 = ( litMat ‘ 𝑊 )
lmatfval.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lmatfval.w ⊢ ( 𝜑 → 𝑊 ∈ Word Word 𝑉 )
lmatfval.1 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑁 )
lmatfval.2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 )
lmatfval.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
lmatfval.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
Assertion lmatfval ( 𝜑 → ( 𝐼 𝑀 𝐽 ) = ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) )

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 lmatfval.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑁 ) )
7 lmatfval.j ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... 𝑁 ) )
8 lmatval ⊢ ( 𝑊 ∈ Word Word 𝑉 → ( litMat ‘ 𝑊 ) = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
9 3 8 syl ⊢ ( 𝜑 → ( litMat ‘ 𝑊 ) = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
10 1 9 syl5eq ⊢ ( 𝜑 → 𝑀 = ( 𝑖 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) , 𝑗 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) ↦ ( ( 𝑊 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) ) )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → 𝑖 = 𝐼 )
12 11 fvoveq1d ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( 𝑊 ‘ ( 𝑖 − 1 ) ) = ( 𝑊 ‘ ( 𝐼 − 1 ) ) )
13 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → 𝑗 = 𝐽 )
14 13 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( 𝑗 − 1 ) = ( 𝐽 − 1 ) )
15 12 14 fveq12d ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → ( ( 𝑊 ‘ ( 𝑖 − 1 ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) )
16 4 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... 𝑁 ) )
17 6 16 eleqtrrd ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
18 1m1e0 ⊢ ( 1 − 1 ) = 0
19 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
20 2 19 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
21 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
22 20 21 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝑁 ) )
23 fz1fzo0m1 ⊢ ( 1 ∈ ( 1 ... 𝑁 ) → ( 1 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
24 22 23 syl ⊢ ( 𝜑 → ( 1 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
25 18 24 eqeltrrid ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑁 ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → 𝑖 = 0 )
27 26 eleq1d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ 0 ∈ ( 0 ..^ 𝑁 ) ) )
28 26 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ 0 ) )
29 28 fveqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ↔ ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 ) )
30 27 29 imbi12d ⊢ ( ( 𝜑 ∧ 𝑖 = 0 ) → ( ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ) ↔ ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 ) ) )
31 5 ex ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ) )
32 25 30 31 vtocld ⊢ ( 𝜑 → ( 0 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 ) )
33 25 32 mpd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ‘ 0 ) ) = 𝑁 )
34 33 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) = ( 1 ... 𝑁 ) )
35 7 34 eleqtrrd ⊢ ( 𝜑 → 𝐽 ∈ ( 1 ... ( ♯ ‘ ( 𝑊 ‘ 0 ) ) ) )
36 fz1fzo0m1 ⊢ ( 𝐼 ∈ ( 1 ... 𝑁 ) → ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
37 6 36 syl ⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
38 4 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝑁 ) )
39 37 38 eleqtrrd ⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
40 wrdsymbcl ⊢ ( ( 𝑊 ∈ Word Word 𝑉 ∧ ( 𝐼 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( 𝐼 − 1 ) ) ∈ Word 𝑉 )
41 3 39 40 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ ( 𝐼 − 1 ) ) ∈ Word 𝑉 )
42 fz1fzo0m1 ⊢ ( 𝐽 ∈ ( 1 ... 𝑁 ) → ( 𝐽 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
43 7 42 syl ⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ( 0 ..^ 𝑁 ) )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝐼 − 1 ) ) → 𝑖 = ( 𝐼 − 1 ) )
45 44 eleq1d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝐼 − 1 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) )
46 44 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝐼 − 1 ) ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ ( 𝐼 − 1 ) ) )
47 46 fveqeq2d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝐼 − 1 ) ) → ( ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ↔ ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) = 𝑁 ) )
48 45 47 imbi12d ⊢ ( ( 𝜑 ∧ 𝑖 = ( 𝐼 − 1 ) ) → ( ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ 𝑖 ) ) = 𝑁 ) ↔ ( ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) = 𝑁 ) ) )
49 37 48 31 vtocld ⊢ ( 𝜑 → ( ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) = 𝑁 ) )
50 37 49 mpd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) = 𝑁 )
51 50 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) ) = ( 0 ..^ 𝑁 ) )
52 43 51 eleqtrrd ⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) ) )
53 wrdsymbcl ⊢ ( ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ∈ Word 𝑉 ∧ ( 𝐽 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) ∈ 𝑉 )
54 41 52 53 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) ∈ 𝑉 )
55 10 15 17 35 54 ovmpod ⊢ ( 𝜑 → ( 𝐼 𝑀 𝐽 ) = ( ( 𝑊 ‘ ( 𝐼 − 1 ) ) ‘ ( 𝐽 − 1 ) ) )