Metamath Proof Explorer

Theorem sseqfv2

Description: Value of the strong sequence builder function. (Contributed by Thierry Arnoux, 21-Apr-2019)

Ref Expression
Hypotheses sseqval.1 
|- ( ph -> S e. _V )
sseqval.2 
|- ( ph -> M e. Word S )
sseqval.3 
|- W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
sseqval.4 
|- ( ph -> F : W --> S )
sseqfv2.4 
|- ( ph -> N e. ( ZZ>= ` ( # ` M ) ) )
Assertion sseqfv2 
|- ( ph -> ( ( M seqstr F ) ` N ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 sseqval.1 
 |-  ( ph -> S e. _V )
2 sseqval.2 
 |-  ( ph -> M e. Word S )
3 sseqval.3 
 |-  W = ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) )
4 sseqval.4 
 |-  ( ph -> F : W --> S )
5 sseqfv2.4 
 |-  ( ph -> N e. ( ZZ>= ` ( # ` M ) ) )
6 1 2 3 4 sseqval 
 |-  ( ph -> ( M seqstr F ) = ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) )
7 6 fveq1d 
 |-  ( ph -> ( ( M seqstr F ) ` N ) = ( ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) ` N ) )
8 wrdfn 
 |-  ( M e. Word S -> M Fn ( 0 ..^ ( # ` M ) ) )
9 2 8 syl 
 |-  ( ph -> M Fn ( 0 ..^ ( # ` M ) ) )
10 fvex 
 |-  ( x ` ( ( # ` x ) - 1 ) ) e. _V
11 df-lsw 
 |-  lastS = ( x e. _V |-> ( x ` ( ( # ` x ) - 1 ) ) )
12 10 11 fnmpti 
 |-  lastS Fn _V
13 12 a1i 
 |-  ( ph -> lastS Fn _V )
14 lencl 
 |-  ( M e. Word S -> ( # ` M ) e. NN0 )
15 2 14 syl 
 |-  ( ph -> ( # ` M ) e. NN0 )
16 15 nn0zd 
 |-  ( ph -> ( # ` M ) e. ZZ )
17 seqfn 
 |-  ( ( # ` M ) e. ZZ -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) )
18 16 17 syl 
 |-  ( ph -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) )
19 ssv 
 |-  ran seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) C_ _V
20 19 a1i 
 |-  ( ph -> ran seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) C_ _V )
21 fnco 
 |-  ( ( lastS Fn _V /\ seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) /\ ran seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) C_ _V ) -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) Fn ( ZZ>= ` ( # ` M ) ) )
22 13 18 20 21 syl3anc 
 |-  ( ph -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) Fn ( ZZ>= ` ( # ` M ) ) )
23 fzouzdisj 
 |-  ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/)
24 23 a1i 
 |-  ( ph -> ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/) )
25 fvun2 
 |-  ( ( M Fn ( 0 ..^ ( # ` M ) ) /\ ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) Fn ( ZZ>= ` ( # ` M ) ) /\ ( ( ( 0 ..^ ( # ` M ) ) i^i ( ZZ>= ` ( # ` M ) ) ) = (/) /\ N e. ( ZZ>= ` ( # ` M ) ) ) ) -> ( ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) ` N ) = ( ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ` N ) )
26 9 22 24 5 25 syl112anc 
 |-  ( ph -> ( ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) ` N ) = ( ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ` N ) )
27 fnfun 
 |-  ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) Fn ( ZZ>= ` ( # ` M ) ) -> Fun seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) )
28 18 27 syl 
 |-  ( ph -> Fun seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) )
29 fvexd 
 |-  ( ph -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` ( # ` M ) ) e. _V )
30 ovexd 
 |-  ( ( ph /\ ( a e. _V /\ b e. _V ) ) -> ( a ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) b ) e. _V )
31 eqid 
 |-  ( ZZ>= ` ( # ` M ) ) = ( ZZ>= ` ( # ` M ) )
32 fvexd 
 |-  ( ( ph /\ a e. ( ZZ>= ` ( ( # ` M ) + 1 ) ) ) -> ( ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ` a ) e. _V )
33 29 30 31 16 32 seqf2 
 |-  ( ph -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) : ( ZZ>= ` ( # ` M ) ) --> _V )
34 33 fdmd 
 |-  ( ph -> dom seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) = ( ZZ>= ` ( # ` M ) ) )
35 5 34 eleqtrrd 
 |-  ( ph -> N e. dom seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) )
36 fvco 
 |-  ( ( Fun seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) /\ N e. dom seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) -> ( ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ` N ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) )
37 28 35 36 syl2anc 
 |-  ( ph -> ( ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ` N ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) )
38 7 26 37 3eqtrd 
 |-  ( ph -> ( ( M seqstr F ) ` N ) = ( lastS ` ( seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ` N ) ) )