Metamath Proof Explorer


Theorem lmatcl

Description: Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-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 )
lmatcl.b
|- V = ( Base ` R )
lmatcl.1
|- O = ( ( 1 ... N ) Mat R )
lmatcl.2
|- P = ( Base ` O )
lmatcl.r
|- ( ph -> R e. X )
Assertion lmatcl
|- ( ph -> M e. P )

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 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 )