Metamath Proof Explorer

Theorem efgsval2

Description: Value of the auxiliary function S defining a sequence of extensions. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
Assertion efgsval2 
|- ( ( A e. Word W /\ B e. W /\ ( A ++ <" B "> ) e. dom S ) -> ( S ` ( A ++ <" B "> ) ) = B )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 1 2 3 4 5 6 efgsval 
 |-  ( ( A ++ <" B "> ) e. dom S -> ( S ` ( A ++ <" B "> ) ) = ( ( A ++ <" B "> ) ` ( ( # ` ( A ++ <" B "> ) ) - 1 ) ) )
8 s1cl 
 |-  ( B e. W -> <" B "> e. Word W )
9 ccatlen 
 |-  ( ( A e. Word W /\ <" B "> e. Word W ) -> ( # ` ( A ++ <" B "> ) ) = ( ( # ` A ) + ( # ` <" B "> ) ) )
10 8 9 sylan2 
 |-  ( ( A e. Word W /\ B e. W ) -> ( # ` ( A ++ <" B "> ) ) = ( ( # ` A ) + ( # ` <" B "> ) ) )
11 s1len 
 |-  ( # ` <" B "> ) = 1
12 11 oveq2i 
 |-  ( ( # ` A ) + ( # ` <" B "> ) ) = ( ( # ` A ) + 1 )
13 10 12 eqtrdi 
 |-  ( ( A e. Word W /\ B e. W ) -> ( # ` ( A ++ <" B "> ) ) = ( ( # ` A ) + 1 ) )
14 13 oveq1d 
 |-  ( ( A e. Word W /\ B e. W ) -> ( ( # ` ( A ++ <" B "> ) ) - 1 ) = ( ( ( # ` A ) + 1 ) - 1 ) )
15 lencl 
 |-  ( A e. Word W -> ( # ` A ) e. NN0 )
16 15 nn0cnd 
 |-  ( A e. Word W -> ( # ` A ) e. CC )
17 ax-1cn 
 |-  1 e. CC
18 pncan 
 |-  ( ( ( # ` A ) e. CC /\ 1 e. CC ) -> ( ( ( # ` A ) + 1 ) - 1 ) = ( # ` A ) )
19 16 17 18 sylancl 
 |-  ( A e. Word W -> ( ( ( # ` A ) + 1 ) - 1 ) = ( # ` A ) )
20 16 addid2d 
 |-  ( A e. Word W -> ( 0 + ( # ` A ) ) = ( # ` A ) )
21 19 20 eqtr4d 
 |-  ( A e. Word W -> ( ( ( # ` A ) + 1 ) - 1 ) = ( 0 + ( # ` A ) ) )
22 21 adantr 
 |-  ( ( A e. Word W /\ B e. W ) -> ( ( ( # ` A ) + 1 ) - 1 ) = ( 0 + ( # ` A ) ) )
23 14 22 eqtrd 
 |-  ( ( A e. Word W /\ B e. W ) -> ( ( # ` ( A ++ <" B "> ) ) - 1 ) = ( 0 + ( # ` A ) ) )
24 23 fveq2d 
 |-  ( ( A e. Word W /\ B e. W ) -> ( ( A ++ <" B "> ) ` ( ( # ` ( A ++ <" B "> ) ) - 1 ) ) = ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) )
25 simpl 
 |-  ( ( A e. Word W /\ B e. W ) -> A e. Word W )
26 8 adantl 
 |-  ( ( A e. Word W /\ B e. W ) -> <" B "> e. Word W )
27 1nn 
 |-  1 e. NN
28 11 27 eqeltri 
 |-  ( # ` <" B "> ) e. NN
29 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` <" B "> ) ) <-> ( # ` <" B "> ) e. NN )
30 28 29 mpbir 
 |-  0 e. ( 0 ..^ ( # ` <" B "> ) )
31 30 a1i 
 |-  ( ( A e. Word W /\ B e. W ) -> 0 e. ( 0 ..^ ( # ` <" B "> ) ) )
32 ccatval3 
 |-  ( ( A e. Word W /\ <" B "> e. Word W /\ 0 e. ( 0 ..^ ( # ` <" B "> ) ) ) -> ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) = ( <" B "> ` 0 ) )
33 25 26 31 32 syl3anc 
 |-  ( ( A e. Word W /\ B e. W ) -> ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) = ( <" B "> ` 0 ) )
34 s1fv 
 |-  ( B e. W -> ( <" B "> ` 0 ) = B )
35 34 adantl 
 |-  ( ( A e. Word W /\ B e. W ) -> ( <" B "> ` 0 ) = B )
36 24 33 35 3eqtrd 
 |-  ( ( A e. Word W /\ B e. W ) -> ( ( A ++ <" B "> ) ` ( ( # ` ( A ++ <" B "> ) ) - 1 ) ) = B )
37 7 36 sylan9eqr 
 |-  ( ( ( A e. Word W /\ B e. W ) /\ ( A ++ <" B "> ) e. dom S ) -> ( S ` ( A ++ <" B "> ) ) = B )
38 37 3impa 
 |-  ( ( A e. Word W /\ B e. W /\ ( A ++ <" B "> ) e. dom S ) -> ( S ` ( A ++ <" B "> ) ) = B )