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