Metamath Proof Explorer

Theorem lmatfval

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

Ref Expression
Hypotheses lmatfval.m ⊢ M = litMat ⁡ W
lmatfval.n ⊢ φ → N ∈ ℕ
lmatfval.w ⊢ φ → W ∈ Word Word V
lmatfval.1 ⊢ φ → W = N
lmatfval.2 ⊢ φ ∧ i ∈ 0 ..^ N → W ⁡ i = N
lmatfval.i ⊢ φ → I ∈ 1 … N
lmatfval.j ⊢ φ → J ∈ 1 … N
Assertion lmatfval ⊢ φ → I M J = W ⁡ I − 1 ⁡ J − 1

Proof

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