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 |
|
lmatcl.b |
|- V = ( Base ` R ) |
7 |
|
lmatcl.1 |
|- O = ( ( 1 ... N ) Mat R ) |
8 |
|
lmatcl.2 |
|- P = ( Base ` O ) |
9 |
|
lmatcl.r |
|- ( ph -> R e. X ) |
10 |
|
lmatval |
|- ( W e. Word Word V -> ( litMat ` W ) = ( k e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) ) |
11 |
3 10
|
syl |
|- ( ph -> ( litMat ` W ) = ( k e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) ) |
12 |
1 11
|
syl5eq |
|- ( ph -> M = ( k e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) ) |
13 |
4
|
oveq2d |
|- ( ph -> ( 1 ... ( # ` W ) ) = ( 1 ... N ) ) |
14 |
|
lbfzo0 |
|- ( 0 e. ( 0 ..^ N ) <-> N e. NN ) |
15 |
2 14
|
sylibr |
|- ( ph -> 0 e. ( 0 ..^ N ) ) |
16 |
|
0nn0 |
|- 0 e. NN0 |
17 |
16
|
a1i |
|- ( ph -> 0 e. NN0 ) |
18 |
|
simpr |
|- ( ( ph /\ i = 0 ) -> i = 0 ) |
19 |
18
|
eleq1d |
|- ( ( ph /\ i = 0 ) -> ( i e. ( 0 ..^ N ) <-> 0 e. ( 0 ..^ N ) ) ) |
20 |
18
|
fveq2d |
|- ( ( ph /\ i = 0 ) -> ( W ` i ) = ( W ` 0 ) ) |
21 |
20
|
fveqeq2d |
|- ( ( ph /\ i = 0 ) -> ( ( # ` ( W ` i ) ) = N <-> ( # ` ( W ` 0 ) ) = N ) ) |
22 |
19 21
|
imbi12d |
|- ( ( ph /\ i = 0 ) -> ( ( i e. ( 0 ..^ N ) -> ( # ` ( W ` i ) ) = N ) <-> ( 0 e. ( 0 ..^ N ) -> ( # ` ( W ` 0 ) ) = N ) ) ) |
23 |
5
|
ex |
|- ( ph -> ( i e. ( 0 ..^ N ) -> ( # ` ( W ` i ) ) = N ) ) |
24 |
17 22 23
|
vtocld |
|- ( ph -> ( 0 e. ( 0 ..^ N ) -> ( # ` ( W ` 0 ) ) = N ) ) |
25 |
15 24
|
mpd |
|- ( ph -> ( # ` ( W ` 0 ) ) = N ) |
26 |
25
|
oveq2d |
|- ( ph -> ( 1 ... ( # ` ( W ` 0 ) ) ) = ( 1 ... N ) ) |
27 |
|
eqidd |
|- ( ph -> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) = ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) |
28 |
13 26 27
|
mpoeq123dv |
|- ( ph -> ( k e. ( 1 ... ( # ` W ) ) , j e. ( 1 ... ( # ` ( W ` 0 ) ) ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) = ( k e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) ) |
29 |
12 28
|
eqtrd |
|- ( ph -> M = ( k e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) ) |
30 |
|
fzfid |
|- ( ph -> ( 1 ... N ) e. Fin ) |
31 |
3
|
3ad2ant1 |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> W e. Word Word V ) |
32 |
|
simp2 |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> k e. ( 1 ... N ) ) |
33 |
|
fz1fzo0m1 |
|- ( k e. ( 1 ... N ) -> ( k - 1 ) e. ( 0 ..^ N ) ) |
34 |
32 33
|
syl |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( k - 1 ) e. ( 0 ..^ N ) ) |
35 |
4
|
3ad2ant1 |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( # ` W ) = N ) |
36 |
35
|
oveq2d |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ N ) ) |
37 |
34 36
|
eleqtrrd |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( k - 1 ) e. ( 0 ..^ ( # ` W ) ) ) |
38 |
|
wrdsymbcl |
|- ( ( W e. Word Word V /\ ( k - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( k - 1 ) ) e. Word V ) |
39 |
31 37 38
|
syl2anc |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( W ` ( k - 1 ) ) e. Word V ) |
40 |
|
simp3 |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) ) |
41 |
|
fz1fzo0m1 |
|- ( j e. ( 1 ... N ) -> ( j - 1 ) e. ( 0 ..^ N ) ) |
42 |
40 41
|
syl |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ..^ N ) ) |
43 |
|
ovexd |
|- ( ph -> ( k - 1 ) e. _V ) |
44 |
|
simpr |
|- ( ( ph /\ i = ( k - 1 ) ) -> i = ( k - 1 ) ) |
45 |
|
eqidd |
|- ( ( ph /\ i = ( k - 1 ) ) -> ( 0 ..^ N ) = ( 0 ..^ N ) ) |
46 |
44 45
|
eleq12d |
|- ( ( ph /\ i = ( k - 1 ) ) -> ( i e. ( 0 ..^ N ) <-> ( k - 1 ) e. ( 0 ..^ N ) ) ) |
47 |
44
|
fveq2d |
|- ( ( ph /\ i = ( k - 1 ) ) -> ( W ` i ) = ( W ` ( k - 1 ) ) ) |
48 |
47
|
fveqeq2d |
|- ( ( ph /\ i = ( k - 1 ) ) -> ( ( # ` ( W ` i ) ) = N <-> ( # ` ( W ` ( k - 1 ) ) ) = N ) ) |
49 |
46 48
|
imbi12d |
|- ( ( ph /\ i = ( k - 1 ) ) -> ( ( i e. ( 0 ..^ N ) -> ( # ` ( W ` i ) ) = N ) <-> ( ( k - 1 ) e. ( 0 ..^ N ) -> ( # ` ( W ` ( k - 1 ) ) ) = N ) ) ) |
50 |
43 49 23
|
vtocld |
|- ( ph -> ( ( k - 1 ) e. ( 0 ..^ N ) -> ( # ` ( W ` ( k - 1 ) ) ) = N ) ) |
51 |
50
|
imp |
|- ( ( ph /\ ( k - 1 ) e. ( 0 ..^ N ) ) -> ( # ` ( W ` ( k - 1 ) ) ) = N ) |
52 |
33 51
|
sylan2 |
|- ( ( ph /\ k e. ( 1 ... N ) ) -> ( # ` ( W ` ( k - 1 ) ) ) = N ) |
53 |
52
|
3adant3 |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( # ` ( W ` ( k - 1 ) ) ) = N ) |
54 |
53
|
oveq2d |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( 0 ..^ ( # ` ( W ` ( k - 1 ) ) ) ) = ( 0 ..^ N ) ) |
55 |
42 54
|
eleqtrrd |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( j - 1 ) e. ( 0 ..^ ( # ` ( W ` ( k - 1 ) ) ) ) ) |
56 |
|
wrdsymbcl |
|- ( ( ( W ` ( k - 1 ) ) e. Word V /\ ( j - 1 ) e. ( 0 ..^ ( # ` ( W ` ( k - 1 ) ) ) ) ) -> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) e. V ) |
57 |
39 55 56
|
syl2anc |
|- ( ( ph /\ k e. ( 1 ... N ) /\ j e. ( 1 ... N ) ) -> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) e. V ) |
58 |
7 6 8 30 9 57
|
matbas2d |
|- ( ph -> ( k e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( W ` ( k - 1 ) ) ` ( j - 1 ) ) ) e. P ) |
59 |
29 58
|
eqeltrd |
|- ( ph -> M e. P ) |