Metamath Proof Explorer

Theorem efgcpbllemb

Description: Lemma for efgrelex . Show that L is an equivalence relation containing all direct extensions of a word, so is closed under .~ . (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 ) ) )
efgcpbllem.1 
|- L = { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
Assertion efgcpbllemb 
|- ( ( A e. W /\ B e. W ) -> .~ C_ L )

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 efgcpbllem.1 
 |-  L = { <. i , j >. | ( { i , j } C_ W /\ ( ( A ++ i ) ++ B ) .~ ( ( A ++ j ) ++ B ) ) }
8 1 2 3 4 efgval2 
 |-  .~ = |^| { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) }
9 7 relopabiv 
 |-  Rel L
10 9 a1i 
 |-  ( ( A e. W /\ B e. W ) -> Rel L )
11 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( f L g <-> ( f e. W /\ g e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ g ) ++ B ) ) )
12 11 simp2bi 
 |-  ( f L g -> g e. W )
13 12 adantl 
 |-  ( ( ( A e. W /\ B e. W ) /\ f L g ) -> g e. W )
14 11 simp1bi 
 |-  ( f L g -> f e. W )
15 14 adantl 
 |-  ( ( ( A e. W /\ B e. W ) /\ f L g ) -> f e. W )
16 1 2 efger 
 |-  .~ Er W
17 16 a1i 
 |-  ( ( ( A e. W /\ B e. W ) /\ f L g ) -> .~ Er W )
18 11 simp3bi 
 |-  ( f L g -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ g ) ++ B ) )
19 18 adantl 
 |-  ( ( ( A e. W /\ B e. W ) /\ f L g ) -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ g ) ++ B ) )
20 17 19 ersym 
 |-  ( ( ( A e. W /\ B e. W ) /\ f L g ) -> ( ( A ++ g ) ++ B ) .~ ( ( A ++ f ) ++ B ) )
21 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( g L f <-> ( g e. W /\ f e. W /\ ( ( A ++ g ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) )
22 13 15 20 21 syl3anbrc 
 |-  ( ( ( A e. W /\ B e. W ) /\ f L g ) -> g L f )
23 14 ad2antrl 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> f e. W )
24 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( g L h <-> ( g e. W /\ h e. W /\ ( ( A ++ g ) ++ B ) .~ ( ( A ++ h ) ++ B ) ) )
25 24 simp2bi 
 |-  ( g L h -> h e. W )
26 25 ad2antll 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> h e. W )
27 16 a1i 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> .~ Er W )
28 18 ad2antrl 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ g ) ++ B ) )
29 24 simp3bi 
 |-  ( g L h -> ( ( A ++ g ) ++ B ) .~ ( ( A ++ h ) ++ B ) )
30 29 ad2antll 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> ( ( A ++ g ) ++ B ) .~ ( ( A ++ h ) ++ B ) )
31 27 28 30 ertrd 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ h ) ++ B ) )
32 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( f L h <-> ( f e. W /\ h e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ h ) ++ B ) ) )
33 23 26 31 32 syl3anbrc 
 |-  ( ( ( A e. W /\ B e. W ) /\ ( f L g /\ g L h ) ) -> f L h )
34 16 a1i 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> .~ Er W )
35 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
36 1 35 eqsstri 
 |-  W C_ Word ( I X. 2o )
37 simpll 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> A e. W )
38 36 37 sselid 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> A e. Word ( I X. 2o ) )
39 simpr 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> f e. W )
40 36 39 sselid 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> f e. Word ( I X. 2o ) )
41 ccatcl 
 |-  ( ( A e. Word ( I X. 2o ) /\ f e. Word ( I X. 2o ) ) -> ( A ++ f ) e. Word ( I X. 2o ) )
42 38 40 41 syl2anc 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( A ++ f ) e. Word ( I X. 2o ) )
43 simplr 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> B e. W )
44 36 43 sselid 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> B e. Word ( I X. 2o ) )
45 ccatcl 
 |-  ( ( ( A ++ f ) e. Word ( I X. 2o ) /\ B e. Word ( I X. 2o ) ) -> ( ( A ++ f ) ++ B ) e. Word ( I X. 2o ) )
46 42 44 45 syl2anc 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( ( A ++ f ) ++ B ) e. Word ( I X. 2o ) )
47 1 efgrcl 
 |-  ( A e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
48 47 simprd 
 |-  ( A e. W -> W = Word ( I X. 2o ) )
49 48 ad2antrr 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> W = Word ( I X. 2o ) )
50 46 49 eleqtrrd 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( ( A ++ f ) ++ B ) e. W )
51 34 50 erref 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) )
52 51 ex 
 |-  ( ( A e. W /\ B e. W ) -> ( f e. W -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) )
53 52 pm4.71d 
 |-  ( ( A e. W /\ B e. W ) -> ( f e. W <-> ( f e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) ) )
54 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( f L f <-> ( f e. W /\ f e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) )
55 df-3an 
 |-  ( ( f e. W /\ f e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) <-> ( ( f e. W /\ f e. W ) /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) )
56 anidm 
 |-  ( ( f e. W /\ f e. W ) <-> f e. W )
57 56 anbi1i 
 |-  ( ( ( f e. W /\ f e. W ) /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) <-> ( f e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) )
58 54 55 57 3bitri 
 |-  ( f L f <-> ( f e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ f ) ++ B ) ) )
59 53 58 bitr4di 
 |-  ( ( A e. W /\ B e. W ) -> ( f e. W <-> f L f ) )
60 10 22 33 59 iserd 
 |-  ( ( A e. W /\ B e. W ) -> L Er W )
61 1 2 3 4 efgtf 
 |-  ( f e. W -> ( ( T ` f ) = ( a e. ( 0 ... ( # ` f ) ) , b e. ( I X. 2o ) |-> ( f splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` f ) : ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) --> W ) )
62 61 simprd 
 |-  ( f e. W -> ( T ` f ) : ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) --> W )
63 62 adantl 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( T ` f ) : ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) --> W )
64 ffn 
 |-  ( ( T ` f ) : ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) --> W -> ( T ` f ) Fn ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) )
65 ovelrn 
 |-  ( ( T ` f ) Fn ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) -> ( a e. ran ( T ` f ) <-> E. c e. ( 0 ... ( # ` f ) ) E. u e. ( I X. 2o ) a = ( c ( T ` f ) u ) ) )
66 63 64 65 3syl 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( a e. ran ( T ` f ) <-> E. c e. ( 0 ... ( # ` f ) ) E. u e. ( I X. 2o ) a = ( c ( T ` f ) u ) ) )
67 simplr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> f e. W )
68 62 ad2antlr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( T ` f ) : ( ( 0 ... ( # ` f ) ) X. ( I X. 2o ) ) --> W )
69 simprl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> c e. ( 0 ... ( # ` f ) ) )
70 simprr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> u e. ( I X. 2o ) )
71 68 69 70 fovcdmd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( c ( T ` f ) u ) e. W )
72 50 adantr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ f ) ++ B ) e. W )
73 37 adantr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> A e. W )
74 36 73 sselid 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> A e. Word ( I X. 2o ) )
75 40 adantr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> f e. Word ( I X. 2o ) )
76 pfxcl 
 |-  ( f e. Word ( I X. 2o ) -> ( f prefix c ) e. Word ( I X. 2o ) )
77 75 76 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( f prefix c ) e. Word ( I X. 2o ) )
78 ccatcl 
 |-  ( ( A e. Word ( I X. 2o ) /\ ( f prefix c ) e. Word ( I X. 2o ) ) -> ( A ++ ( f prefix c ) ) e. Word ( I X. 2o ) )
79 74 77 78 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( A ++ ( f prefix c ) ) e. Word ( I X. 2o ) )
80 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
81 80 ffvelcdmi 
 |-  ( u e. ( I X. 2o ) -> ( M ` u ) e. ( I X. 2o ) )
82 81 ad2antll 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( M ` u ) e. ( I X. 2o ) )
83 70 82 s2cld 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> <" u ( M ` u ) "> e. Word ( I X. 2o ) )
84 ccatcl 
 |-  ( ( ( A ++ ( f prefix c ) ) e. Word ( I X. 2o ) /\ <" u ( M ` u ) "> e. Word ( I X. 2o ) ) -> ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) e. Word ( I X. 2o ) )
85 79 83 84 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) e. Word ( I X. 2o ) )
86 swrdcl 
 |-  ( f e. Word ( I X. 2o ) -> ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) )
87 75 86 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) )
88 44 adantr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> B e. Word ( I X. 2o ) )
89 ccatass 
 |-  ( ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) e. Word ( I X. 2o ) /\ ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) /\ B e. Word ( I X. 2o ) ) -> ( ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) ++ B ) = ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
90 85 87 88 89 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) ++ B ) = ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
91 ccatcl 
 |-  ( ( ( f prefix c ) e. Word ( I X. 2o ) /\ <" u ( M ` u ) "> e. Word ( I X. 2o ) ) -> ( ( f prefix c ) ++ <" u ( M ` u ) "> ) e. Word ( I X. 2o ) )
92 77 83 91 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( f prefix c ) ++ <" u ( M ` u ) "> ) e. Word ( I X. 2o ) )
93 ccatass 
 |-  ( ( A e. Word ( I X. 2o ) /\ ( ( f prefix c ) ++ <" u ( M ` u ) "> ) e. Word ( I X. 2o ) /\ ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) ) -> ( ( A ++ ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( A ++ ( ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) ) )
94 74 92 87 93 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( A ++ ( ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) ) )
95 ccatass 
 |-  ( ( A e. Word ( I X. 2o ) /\ ( f prefix c ) e. Word ( I X. 2o ) /\ <" u ( M ` u ) "> e. Word ( I X. 2o ) ) -> ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) = ( A ++ ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ) )
96 74 77 83 95 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) = ( A ++ ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ) )
97 96 oveq1d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( ( A ++ ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) )
98 1 2 3 4 efgtval 
 |-  ( ( f e. W /\ c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) -> ( c ( T ` f ) u ) = ( f splice <. c , c , <" u ( M ` u ) "> >. ) )
99 67 69 70 98 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( c ( T ` f ) u ) = ( f splice <. c , c , <" u ( M ` u ) "> >. ) )
100 splval 
 |-  ( ( f e. W /\ ( c e. ( 0 ... ( # ` f ) ) /\ c e. ( 0 ... ( # ` f ) ) /\ <" u ( M ` u ) "> e. Word ( I X. 2o ) ) ) -> ( f splice <. c , c , <" u ( M ` u ) "> >. ) = ( ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) )
101 67 69 69 83 100 syl13anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( f splice <. c , c , <" u ( M ` u ) "> >. ) = ( ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) )
102 99 101 eqtrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( c ( T ` f ) u ) = ( ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) )
103 102 oveq2d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( A ++ ( c ( T ` f ) u ) ) = ( A ++ ( ( ( f prefix c ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) ) )
104 94 97 103 3eqtr4rd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( A ++ ( c ( T ` f ) u ) ) = ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) )
105 104 oveq1d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) = ( ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( f substr <. c , ( # ` f ) >. ) ) ++ B ) )
106 lencl 
 |-  ( A e. Word ( I X. 2o ) -> ( # ` A ) e. NN0 )
107 74 106 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` A ) e. NN0 )
108 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
109 107 108 eleqtrdi 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` A ) e. ( ZZ>= ` 0 ) )
110 elfznn0 
 |-  ( c e. ( 0 ... ( # ` f ) ) -> c e. NN0 )
111 110 ad2antrl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> c e. NN0 )
112 uzaddcl 
 |-  ( ( ( # ` A ) e. ( ZZ>= ` 0 ) /\ c e. NN0 ) -> ( ( # ` A ) + c ) e. ( ZZ>= ` 0 ) )
113 109 111 112 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + c ) e. ( ZZ>= ` 0 ) )
114 42 adantr 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( A ++ f ) e. Word ( I X. 2o ) )
115 ccatlen 
 |-  ( ( ( A ++ f ) e. Word ( I X. 2o ) /\ B e. Word ( I X. 2o ) ) -> ( # ` ( ( A ++ f ) ++ B ) ) = ( ( # ` ( A ++ f ) ) + ( # ` B ) ) )
116 114 88 115 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` ( ( A ++ f ) ++ B ) ) = ( ( # ` ( A ++ f ) ) + ( # ` B ) ) )
117 ccatlen 
 |-  ( ( A e. Word ( I X. 2o ) /\ f e. Word ( I X. 2o ) ) -> ( # ` ( A ++ f ) ) = ( ( # ` A ) + ( # ` f ) ) )
118 74 75 117 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` ( A ++ f ) ) = ( ( # ` A ) + ( # ` f ) ) )
119 elfzuz3 
 |-  ( c e. ( 0 ... ( # ` f ) ) -> ( # ` f ) e. ( ZZ>= ` c ) )
120 119 ad2antrl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` f ) e. ( ZZ>= ` c ) )
121 107 nn0zd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` A ) e. ZZ )
122 eluzadd 
 |-  ( ( ( # ` f ) e. ( ZZ>= ` c ) /\ ( # ` A ) e. ZZ ) -> ( ( # ` f ) + ( # ` A ) ) e. ( ZZ>= ` ( c + ( # ` A ) ) ) )
123 120 121 122 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` f ) + ( # ` A ) ) e. ( ZZ>= ` ( c + ( # ` A ) ) ) )
124 lencl 
 |-  ( f e. Word ( I X. 2o ) -> ( # ` f ) e. NN0 )
125 75 124 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` f ) e. NN0 )
126 125 nn0cnd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` f ) e. CC )
127 107 nn0cnd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` A ) e. CC )
128 126 127 addcomd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` f ) + ( # ` A ) ) = ( ( # ` A ) + ( # ` f ) ) )
129 111 nn0cnd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> c e. CC )
130 129 127 addcomd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( c + ( # ` A ) ) = ( ( # ` A ) + c ) )
131 130 fveq2d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ZZ>= ` ( c + ( # ` A ) ) ) = ( ZZ>= ` ( ( # ` A ) + c ) ) )
132 123 128 131 3eltr3d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + ( # ` f ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) )
133 118 132 eqeltrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` ( A ++ f ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) )
134 lencl 
 |-  ( B e. Word ( I X. 2o ) -> ( # ` B ) e. NN0 )
135 88 134 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` B ) e. NN0 )
136 uzaddcl 
 |-  ( ( ( # ` ( A ++ f ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) /\ ( # ` B ) e. NN0 ) -> ( ( # ` ( A ++ f ) ) + ( # ` B ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) )
137 133 135 136 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` ( A ++ f ) ) + ( # ` B ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) )
138 116 137 eqeltrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` ( ( A ++ f ) ++ B ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) )
139 elfzuzb 
 |-  ( ( ( # ` A ) + c ) e. ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) <-> ( ( ( # ` A ) + c ) e. ( ZZ>= ` 0 ) /\ ( # ` ( ( A ++ f ) ++ B ) ) e. ( ZZ>= ` ( ( # ` A ) + c ) ) ) )
140 113 138 139 sylanbrc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + c ) e. ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) )
141 1 2 3 4 efgtval 
 |-  ( ( ( ( A ++ f ) ++ B ) e. W /\ ( ( # ` A ) + c ) e. ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) /\ u e. ( I X. 2o ) ) -> ( ( ( # ` A ) + c ) ( T ` ( ( A ++ f ) ++ B ) ) u ) = ( ( ( A ++ f ) ++ B ) splice <. ( ( # ` A ) + c ) , ( ( # ` A ) + c ) , <" u ( M ` u ) "> >. ) )
142 72 140 70 141 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( # ` A ) + c ) ( T ` ( ( A ++ f ) ++ B ) ) u ) = ( ( ( A ++ f ) ++ B ) splice <. ( ( # ` A ) + c ) , ( ( # ` A ) + c ) , <" u ( M ` u ) "> >. ) )
143 wrd0 
 |-  (/) e. Word ( I X. 2o )
144 143 a1i 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> (/) e. Word ( I X. 2o ) )
145 ccatcl 
 |-  ( ( ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) /\ B e. Word ( I X. 2o ) ) -> ( ( f substr <. c , ( # ` f ) >. ) ++ B ) e. Word ( I X. 2o ) )
146 87 88 145 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( f substr <. c , ( # ` f ) >. ) ++ B ) e. Word ( I X. 2o ) )
147 ccatrid 
 |-  ( ( A ++ ( f prefix c ) ) e. Word ( I X. 2o ) -> ( ( A ++ ( f prefix c ) ) ++ (/) ) = ( A ++ ( f prefix c ) ) )
148 79 147 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( f prefix c ) ) ++ (/) ) = ( A ++ ( f prefix c ) ) )
149 148 oveq1d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( A ++ ( f prefix c ) ) ++ (/) ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) = ( ( A ++ ( f prefix c ) ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
150 ccatass 
 |-  ( ( ( A ++ ( f prefix c ) ) e. Word ( I X. 2o ) /\ ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) /\ B e. Word ( I X. 2o ) ) -> ( ( ( A ++ ( f prefix c ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) ++ B ) = ( ( A ++ ( f prefix c ) ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
151 79 87 88 150 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( A ++ ( f prefix c ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) ++ B ) = ( ( A ++ ( f prefix c ) ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
152 ccatass 
 |-  ( ( A e. Word ( I X. 2o ) /\ ( f prefix c ) e. Word ( I X. 2o ) /\ ( f substr <. c , ( # ` f ) >. ) e. Word ( I X. 2o ) ) -> ( ( A ++ ( f prefix c ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( A ++ ( ( f prefix c ) ++ ( f substr <. c , ( # ` f ) >. ) ) ) )
153 74 77 87 152 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( f prefix c ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( A ++ ( ( f prefix c ) ++ ( f substr <. c , ( # ` f ) >. ) ) ) )
154 125 108 eleqtrdi 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` f ) e. ( ZZ>= ` 0 ) )
155 eluzfz2 
 |-  ( ( # ` f ) e. ( ZZ>= ` 0 ) -> ( # ` f ) e. ( 0 ... ( # ` f ) ) )
156 154 155 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` f ) e. ( 0 ... ( # ` f ) ) )
157 ccatpfx 
 |-  ( ( f e. Word ( I X. 2o ) /\ c e. ( 0 ... ( # ` f ) ) /\ ( # ` f ) e. ( 0 ... ( # ` f ) ) ) -> ( ( f prefix c ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( f prefix ( # ` f ) ) )
158 75 69 156 157 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( f prefix c ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( f prefix ( # ` f ) ) )
159 pfxid 
 |-  ( f e. Word ( I X. 2o ) -> ( f prefix ( # ` f ) ) = f )
160 75 159 syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( f prefix ( # ` f ) ) = f )
161 158 160 eqtrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( f prefix c ) ++ ( f substr <. c , ( # ` f ) >. ) ) = f )
162 161 oveq2d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( A ++ ( ( f prefix c ) ++ ( f substr <. c , ( # ` f ) >. ) ) ) = ( A ++ f ) )
163 153 162 eqtrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( f prefix c ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) = ( A ++ f ) )
164 163 oveq1d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( A ++ ( f prefix c ) ) ++ ( f substr <. c , ( # ` f ) >. ) ) ++ B ) = ( ( A ++ f ) ++ B ) )
165 149 151 164 3eqtr2rd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ f ) ++ B ) = ( ( ( A ++ ( f prefix c ) ) ++ (/) ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
166 ccatlen 
 |-  ( ( A e. Word ( I X. 2o ) /\ ( f prefix c ) e. Word ( I X. 2o ) ) -> ( # ` ( A ++ ( f prefix c ) ) ) = ( ( # ` A ) + ( # ` ( f prefix c ) ) ) )
167 74 77 166 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` ( A ++ ( f prefix c ) ) ) = ( ( # ` A ) + ( # ` ( f prefix c ) ) ) )
168 pfxlen 
 |-  ( ( f e. Word ( I X. 2o ) /\ c e. ( 0 ... ( # ` f ) ) ) -> ( # ` ( f prefix c ) ) = c )
169 75 69 168 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( # ` ( f prefix c ) ) = c )
170 169 oveq2d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + ( # ` ( f prefix c ) ) ) = ( ( # ` A ) + c ) )
171 167 170 eqtr2d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + c ) = ( # ` ( A ++ ( f prefix c ) ) ) )
172 hash0 
 |-  ( # ` (/) ) = 0
173 172 oveq2i 
 |-  ( ( ( # ` A ) + c ) + ( # ` (/) ) ) = ( ( ( # ` A ) + c ) + 0 )
174 107 111 nn0addcld 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + c ) e. NN0 )
175 174 nn0cnd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + c ) e. CC )
176 175 addridd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( # ` A ) + c ) + 0 ) = ( ( # ` A ) + c ) )
177 173 176 eqtr2id 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( # ` A ) + c ) = ( ( ( # ` A ) + c ) + ( # ` (/) ) ) )
178 79 144 146 83 165 171 177 splval2 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( A ++ f ) ++ B ) splice <. ( ( # ` A ) + c ) , ( ( # ` A ) + c ) , <" u ( M ` u ) "> >. ) = ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
179 142 178 eqtrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( # ` A ) + c ) ( T ` ( ( A ++ f ) ++ B ) ) u ) = ( ( ( A ++ ( f prefix c ) ) ++ <" u ( M ` u ) "> ) ++ ( ( f substr <. c , ( # ` f ) >. ) ++ B ) ) )
180 90 105 179 3eqtr4d 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) = ( ( ( # ` A ) + c ) ( T ` ( ( A ++ f ) ++ B ) ) u ) )
181 1 2 3 4 efgtf 
 |-  ( ( ( A ++ f ) ++ B ) e. W -> ( ( T ` ( ( A ++ f ) ++ B ) ) = ( a e. ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) , b e. ( I X. 2o ) |-> ( ( ( A ++ f ) ++ B ) splice <. a , a , <" b ( M ` b ) "> >. ) ) /\ ( T ` ( ( A ++ f ) ++ B ) ) : ( ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) X. ( I X. 2o ) ) --> W ) )
182 181 simprd 
 |-  ( ( ( A ++ f ) ++ B ) e. W -> ( T ` ( ( A ++ f ) ++ B ) ) : ( ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) X. ( I X. 2o ) ) --> W )
183 ffn 
 |-  ( ( T ` ( ( A ++ f ) ++ B ) ) : ( ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) X. ( I X. 2o ) ) --> W -> ( T ` ( ( A ++ f ) ++ B ) ) Fn ( ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) X. ( I X. 2o ) ) )
184 72 182 183 3syl 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( T ` ( ( A ++ f ) ++ B ) ) Fn ( ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) X. ( I X. 2o ) ) )
185 fnovrn 
 |-  ( ( ( T ` ( ( A ++ f ) ++ B ) ) Fn ( ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) X. ( I X. 2o ) ) /\ ( ( # ` A ) + c ) e. ( 0 ... ( # ` ( ( A ++ f ) ++ B ) ) ) /\ u e. ( I X. 2o ) ) -> ( ( ( # ` A ) + c ) ( T ` ( ( A ++ f ) ++ B ) ) u ) e. ran ( T ` ( ( A ++ f ) ++ B ) ) )
186 184 140 70 185 syl3anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( ( # ` A ) + c ) ( T ` ( ( A ++ f ) ++ B ) ) u ) e. ran ( T ` ( ( A ++ f ) ++ B ) ) )
187 180 186 eqeltrd 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) e. ran ( T ` ( ( A ++ f ) ++ B ) ) )
188 1 2 3 4 efgi2 
 |-  ( ( ( ( A ++ f ) ++ B ) e. W /\ ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) e. ran ( T ` ( ( A ++ f ) ++ B ) ) ) -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) )
189 72 187 188 syl2anc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( ( A ++ f ) ++ B ) .~ ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) )
190 1 2 3 4 5 6 7 efgcpbllema 
 |-  ( f L ( c ( T ` f ) u ) <-> ( f e. W /\ ( c ( T ` f ) u ) e. W /\ ( ( A ++ f ) ++ B ) .~ ( ( A ++ ( c ( T ` f ) u ) ) ++ B ) ) )
191 67 71 189 190 syl3anbrc 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> f L ( c ( T ` f ) u ) )
192 vex 
 |-  a e. _V
193 vex 
 |-  f e. _V
194 192 193 elec 
 |-  ( a e. [ f ] L <-> f L a )
195 breq2 
 |-  ( a = ( c ( T ` f ) u ) -> ( f L a <-> f L ( c ( T ` f ) u ) ) )
196 194 195 bitrid 
 |-  ( a = ( c ( T ` f ) u ) -> ( a e. [ f ] L <-> f L ( c ( T ` f ) u ) ) )
197 191 196 syl5ibrcom 
 |-  ( ( ( ( A e. W /\ B e. W ) /\ f e. W ) /\ ( c e. ( 0 ... ( # ` f ) ) /\ u e. ( I X. 2o ) ) ) -> ( a = ( c ( T ` f ) u ) -> a e. [ f ] L ) )
198 197 rexlimdvva 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( E. c e. ( 0 ... ( # ` f ) ) E. u e. ( I X. 2o ) a = ( c ( T ` f ) u ) -> a e. [ f ] L ) )
199 66 198 sylbid 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ( a e. ran ( T ` f ) -> a e. [ f ] L ) )
200 199 ssrdv 
 |-  ( ( ( A e. W /\ B e. W ) /\ f e. W ) -> ran ( T ` f ) C_ [ f ] L )
201 200 ralrimiva 
 |-  ( ( A e. W /\ B e. W ) -> A. f e. W ran ( T ` f ) C_ [ f ] L )
202 1 fvexi 
 |-  W e. _V
203 erex 
 |-  ( L Er W -> ( W e. _V -> L e. _V ) )
204 60 202 203 mpisyl 
 |-  ( ( A e. W /\ B e. W ) -> L e. _V )
205 ereq1 
 |-  ( r = L -> ( r Er W <-> L Er W ) )
206 eceq2 
 |-  ( r = L -> [ f ] r = [ f ] L )
207 206 sseq2d 
 |-  ( r = L -> ( ran ( T ` f ) C_ [ f ] r <-> ran ( T ` f ) C_ [ f ] L ) )
208 207 ralbidv 
 |-  ( r = L -> ( A. f e. W ran ( T ` f ) C_ [ f ] r <-> A. f e. W ran ( T ` f ) C_ [ f ] L ) )
209 205 208 anbi12d 
 |-  ( r = L -> ( ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) <-> ( L Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] L ) ) )
210 209 elabg 
 |-  ( L e. _V -> ( L e. { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) } <-> ( L Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] L ) ) )
211 204 210 syl 
 |-  ( ( A e. W /\ B e. W ) -> ( L e. { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) } <-> ( L Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] L ) ) )
212 60 201 211 mpbir2and 
 |-  ( ( A e. W /\ B e. W ) -> L e. { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) } )
213 intss1 
 |-  ( L e. { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) } -> |^| { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) } C_ L )
214 212 213 syl 
 |-  ( ( A e. W /\ B e. W ) -> |^| { r | ( r Er W /\ A. f e. W ran ( T ` f ) C_ [ f ] r ) } C_ L )
215 8 214 eqsstrid 
 |-  ( ( A e. W /\ B e. W ) -> .~ C_ L )