Metamath Proof Explorer

Theorem sseqval

Description: Value of the strong sequence builder function. The set W represents here the words of length greater than or equal to the lenght of the initial sequence M . (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 )
Assertion 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 ) "> ) } ) ) ) ) )

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 df-sseq 
 |-  seqstr = ( m e. _V , f e. _V |-> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) )
6 5 a1i 
 |-  ( ph -> seqstr = ( m e. _V , f e. _V |-> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) ) )
7 simprl 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> m = M )
8 7 fveq2d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( # ` m ) = ( # ` M ) )
9 simp1rr 
 |-  ( ( ( ph /\ ( m = M /\ f = F ) ) /\ x e. _V /\ y e. _V ) -> f = F )
10 9 fveq1d 
 |-  ( ( ( ph /\ ( m = M /\ f = F ) ) /\ x e. _V /\ y e. _V ) -> ( f ` x ) = ( F ` x ) )
11 10 s1eqd 
 |-  ( ( ( ph /\ ( m = M /\ f = F ) ) /\ x e. _V /\ y e. _V ) -> <" ( f ` x ) "> = <" ( F ` x ) "> )
12 11 oveq2d 
 |-  ( ( ( ph /\ ( m = M /\ f = F ) ) /\ x e. _V /\ y e. _V ) -> ( x ++ <" ( f ` x ) "> ) = ( x ++ <" ( F ` x ) "> ) )
13 12 mpoeq3dva 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) = ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) )
14 simprr 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> f = F )
15 14 7 fveq12d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( f ` m ) = ( F ` M ) )
16 15 s1eqd 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> <" ( f ` m ) "> = <" ( F ` M ) "> )
17 7 16 oveq12d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( m ++ <" ( f ` m ) "> ) = ( M ++ <" ( F ` M ) "> ) )
18 17 sneqd 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> { ( m ++ <" ( f ` m ) "> ) } = { ( M ++ <" ( F ` M ) "> ) } )
19 18 xpeq2d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) = ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) )
20 8 13 19 seqeq123d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) = seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) )
21 20 coeq2d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( lastS o. 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 ) "> ) } ) ) ) )
22 7 21 uneq12d 
 |-  ( ( ph /\ ( m = M /\ f = F ) ) -> ( m u. ( lastS o. seq ( # ` m ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( f ` x ) "> ) ) , ( NN0 X. { ( m ++ <" ( f ` m ) "> ) } ) ) ) ) = ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) )
23 elex 
 |-  ( M e. Word S -> M e. _V )
24 2 23 syl 
 |-  ( ph -> M e. _V )
25 wrdexg 
 |-  ( S e. _V -> Word S e. _V )
26 inex1g 
 |-  ( Word S e. _V -> ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) e. _V )
27 1 25 26 3syl 
 |-  ( ph -> ( Word S i^i ( `' # " ( ZZ>= ` ( # ` M ) ) ) ) e. _V )
28 3 27 eqeltrid 
 |-  ( ph -> W e. _V )
29 4 28 fexd 
 |-  ( ph -> F e. _V )
30 df-lsw 
 |-  lastS = ( x e. _V |-> ( x ` ( ( # ` x ) - 1 ) ) )
31 30 funmpt2 
 |-  Fun lastS
32 31 a1i 
 |-  ( ph -> Fun lastS )
33 seqex 
 |-  seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) e. _V
34 33 a1i 
 |-  ( ph -> seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) e. _V )
35 cofunexg 
 |-  ( ( Fun lastS /\ seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) e. _V ) -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) e. _V )
36 32 34 35 syl2anc 
 |-  ( ph -> ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) e. _V )
37 unexg 
 |-  ( ( M e. _V /\ ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) e. _V ) -> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) e. _V )
38 24 36 37 syl2anc 
 |-  ( ph -> ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) e. _V )
39 6 22 24 29 38 ovmpod 
 |-  ( ph -> ( M seqstr F ) = ( M u. ( lastS o. seq ( # ` M ) ( ( x e. _V , y e. _V |-> ( x ++ <" ( F ` x ) "> ) ) , ( NN0 X. { ( M ++ <" ( F ` M ) "> ) } ) ) ) ) )