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 
|- ( ph -> N e. NN )
lmatfval.w 
|- ( ph -> W e. Word Word V )
lmatfval.1 
|- ( ph -> ( # ` W ) = N )
lmatfval.2 
|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( # ` ( W ` i ) ) = N )
lmatfval.i 
|- ( ph -> I e. ( 1 ... N ) )
lmatfval.j 
|- ( ph -> J e. ( 1 ... N ) )
Assertion lmatfval 
|- ( ph -> ( I M J ) = ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) )

Proof

Step Hyp Ref Expression
1 lmatfval.m 
 |-  M = ( litMat ` W )
2 lmatfval.n 
 |-  ( ph -> N e. NN )
3 lmatfval.w 
 |-  ( ph -> W e. Word Word V )
4 lmatfval.1 
 |-  ( ph -> ( # ` W ) = N )
5 lmatfval.2 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( # ` ( W ` i ) ) = N )
6 lmatfval.i 
 |-  ( ph -> I e. ( 1 ... N ) )
7 lmatfval.j 
 |-  ( ph -> J e. ( 1 ... N ) )
8 lmatval 
 |-  ( W e. Word Word V -> ( litMat ` W ) = ( i e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
9 3 8 syl 
 |-  ( ph -> ( litMat ` W ) = ( i e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
10 1 9 syl5eq 
 |-  ( ph -> M = ( i e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
11 simprl 
 |-  ( ( ph /\ ( i = I /\ j = J ) ) -> i = I )
12 11 fvoveq1d 
 |-  ( ( ph /\ ( i = I /\ j = J ) ) -> ( W ` ( i - 1 ) ) = ( W ` ( I - 1 ) ) )
13 simprr 
 |-  ( ( ph /\ ( i = I /\ j = J ) ) -> j = J )
14 13 oveq1d 
 |-  ( ( ph /\ ( i = I /\ j = J ) ) -> ( j - 1 ) = ( J - 1 ) )
15 12 14 fveq12d 
 |-  ( ( ph /\ ( i = I /\ j = J ) ) -> ( ( W ` ( i - 1 ) ) ` ( j - 1 ) ) = ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) )
16 4 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` W ) ) = ( 1 ... N ) )
17 6 16 eleqtrrd 
 |-  ( ph -> I e. ( 1 ... ( # ` W ) ) )
18 1m1e0 
 |-  ( 1 - 1 ) = 0
19 nnuz 
 |-  NN = ( ZZ>= ` 1 )
20 2 19 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
21 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
22 20 21 syl 
 |-  ( ph -> 1 e. ( 1 ... N ) )
23 fz1fzo0m1 
 |-  ( 1 e. ( 1 ... N ) -> ( 1 - 1 ) e. ( 0 ..^ N ) )
24 22 23 syl 
 |-  ( ph -> ( 1 - 1 ) e. ( 0 ..^ N ) )
25 18 24 eqeltrrid 
 |-  ( ph -> 0 e. ( 0 ..^ N ) )
26 simpr 
 |-  ( ( ph /\ i = 0 ) -> i = 0 )
27 26 eleq1d 
 |-  ( ( ph /\ i = 0 ) -> ( i e. ( 0 ..^ N ) <-> 0 e. ( 0 ..^ N ) ) )
28 26 fveq2d 
 |-  ( ( ph /\ i = 0 ) -> ( W ` i ) = ( W ` 0 ) )
29 28 fveqeq2d 
 |-  ( ( ph /\ i = 0 ) -> ( ( # ` ( W ` i ) ) = N <-> ( # ` ( W ` 0 ) ) = N ) )
30 27 29 imbi12d 
 |-  ( ( ph /\ i = 0 ) -> ( ( i e. ( 0 ..^ N ) -> ( # ` ( W ` i ) ) = N ) <-> ( 0 e. ( 0 ..^ N ) -> ( # ` ( W ` 0 ) ) = N ) ) )
31 5 ex 
 |-  ( ph -> ( i e. ( 0 ..^ N ) -> ( # ` ( W ` i ) ) = N ) )
32 25 30 31 vtocld 
 |-  ( ph -> ( 0 e. ( 0 ..^ N ) -> ( # ` ( W ` 0 ) ) = N ) )
33 25 32 mpd 
 |-  ( ph -> ( # ` ( W ` 0 ) ) = N )
34 33 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` ( W ` 0 ) ) ) = ( 1 ... N ) )
35 7 34 eleqtrrd 
 |-  ( ph -> J e. ( 1 ... ( # ` ( W ` 0 ) ) ) )
36 fz1fzo0m1 
 |-  ( I e. ( 1 ... N ) -> ( I - 1 ) e. ( 0 ..^ N ) )
37 6 36 syl 
 |-  ( ph -> ( I - 1 ) e. ( 0 ..^ N ) )
38 4 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ N ) )
39 37 38 eleqtrrd 
 |-  ( ph -> ( I - 1 ) e. ( 0 ..^ ( # ` W ) ) )
40 wrdsymbcl 
 |-  ( ( W e. Word Word V /\ ( I - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( I - 1 ) ) e. Word V )
41 3 39 40 syl2anc 
 |-  ( ph -> ( W ` ( I - 1 ) ) e. Word V )
42 fz1fzo0m1 
 |-  ( J e. ( 1 ... N ) -> ( J - 1 ) e. ( 0 ..^ N ) )
43 7 42 syl 
 |-  ( ph -> ( J - 1 ) e. ( 0 ..^ N ) )
44 simpr 
 |-  ( ( ph /\ i = ( I - 1 ) ) -> i = ( I - 1 ) )
45 44 eleq1d 
 |-  ( ( ph /\ i = ( I - 1 ) ) -> ( i e. ( 0 ..^ N ) <-> ( I - 1 ) e. ( 0 ..^ N ) ) )
46 44 fveq2d 
 |-  ( ( ph /\ i = ( I - 1 ) ) -> ( W ` i ) = ( W ` ( I - 1 ) ) )
47 46 fveqeq2d 
 |-  ( ( ph /\ i = ( I - 1 ) ) -> ( ( # ` ( W ` i ) ) = N <-> ( # ` ( W ` ( I - 1 ) ) ) = N ) )
48 45 47 imbi12d 
 |-  ( ( ph /\ i = ( I - 1 ) ) -> ( ( i e. ( 0 ..^ N ) -> ( # ` ( W ` i ) ) = N ) <-> ( ( I - 1 ) e. ( 0 ..^ N ) -> ( # ` ( W ` ( I - 1 ) ) ) = N ) ) )
49 37 48 31 vtocld 
 |-  ( ph -> ( ( I - 1 ) e. ( 0 ..^ N ) -> ( # ` ( W ` ( I - 1 ) ) ) = N ) )
50 37 49 mpd 
 |-  ( ph -> ( # ` ( W ` ( I - 1 ) ) ) = N )
51 50 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` ( W ` ( I - 1 ) ) ) ) = ( 0 ..^ N ) )
52 43 51 eleqtrrd 
 |-  ( ph -> ( J - 1 ) e. ( 0 ..^ ( # ` ( W ` ( I - 1 ) ) ) ) )
53 wrdsymbcl 
 |-  ( ( ( W ` ( I - 1 ) ) e. Word V /\ ( J - 1 ) e. ( 0 ..^ ( # ` ( W ` ( I - 1 ) ) ) ) ) -> ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) e. V )
54 41 52 53 syl2anc 
 |-  ( ph -> ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) e. V )
55 10 15 17 35 54 ovmpod 
 |-  ( ph -> ( I M J ) = ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) )