Metamath Proof Explorer

Theorem efgredlemg

Description: Lemma for efgred . (Contributed by Mario Carneiro, 4-Jun-2016)

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 ) ) )
efgredlem.1 
|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
efgredlem.2 
|- ( ph -> A e. dom S )
efgredlem.3 
|- ( ph -> B e. dom S )
efgredlem.4 
|- ( ph -> ( S ` A ) = ( S ` B ) )
efgredlem.5 
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
efgredlemb.k 
|- K = ( ( ( # ` A ) - 1 ) - 1 )
efgredlemb.l 
|- L = ( ( ( # ` B ) - 1 ) - 1 )
efgredlemb.p 
|- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
efgredlemb.q 
|- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
efgredlemb.u 
|- ( ph -> U e. ( I X. 2o ) )
efgredlemb.v 
|- ( ph -> V e. ( I X. 2o ) )
efgredlemb.6 
|- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
efgredlemb.7 
|- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
Assertion efgredlemg 
|- ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` 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 efgredlem.1 
 |-  ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
8 efgredlem.2 
 |-  ( ph -> A e. dom S )
9 efgredlem.3 
 |-  ( ph -> B e. dom S )
10 efgredlem.4 
 |-  ( ph -> ( S ` A ) = ( S ` B ) )
11 efgredlem.5 
 |-  ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
12 efgredlemb.k 
 |-  K = ( ( ( # ` A ) - 1 ) - 1 )
13 efgredlemb.l 
 |-  L = ( ( ( # ` B ) - 1 ) - 1 )
14 efgredlemb.p 
 |-  ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
15 efgredlemb.q 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
16 efgredlemb.u 
 |-  ( ph -> U e. ( I X. 2o ) )
17 efgredlemb.v 
 |-  ( ph -> V e. ( I X. 2o ) )
18 efgredlemb.6 
 |-  ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
19 efgredlemb.7 
 |-  ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
20 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
21 1 20 eqsstri 
 |-  W C_ Word ( I X. 2o )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 efgredlemf 
 |-  ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) )
23 22 simpld 
 |-  ( ph -> ( A ` K ) e. W )
24 21 23 sselid 
 |-  ( ph -> ( A ` K ) e. Word ( I X. 2o ) )
25 lencl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( # ` ( A ` K ) ) e. NN0 )
26 24 25 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. NN0 )
27 26 nn0cnd 
 |-  ( ph -> ( # ` ( A ` K ) ) e. CC )
28 22 simprd 
 |-  ( ph -> ( B ` L ) e. W )
29 21 28 sselid 
 |-  ( ph -> ( B ` L ) e. Word ( I X. 2o ) )
30 lencl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 )
31 29 30 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. NN0 )
32 31 nn0cnd 
 |-  ( ph -> ( # ` ( B ` L ) ) e. CC )
33 2cnd 
 |-  ( ph -> 2 e. CC )
34 1 2 3 4 5 6 7 8 9 10 11 efgredlema 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
35 34 simpld 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. NN )
36 1 2 3 4 5 6 efgsdmi 
 |-  ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. NN ) -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
37 8 35 36 syl2anc 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
38 12 fveq2i 
 |-  ( A ` K ) = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) )
39 38 fveq2i 
 |-  ( T ` ( A ` K ) ) = ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
40 39 rneqi 
 |-  ran ( T ` ( A ` K ) ) = ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
41 37 40 eleqtrrdi 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( A ` K ) ) )
42 1 2 3 4 efgtlen 
 |-  ( ( ( A ` K ) e. W /\ ( S ` A ) e. ran ( T ` ( A ` K ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` K ) ) + 2 ) )
43 23 41 42 syl2anc 
 |-  ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` K ) ) + 2 ) )
44 34 simprd 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. NN )
45 1 2 3 4 5 6 efgsdmi 
 |-  ( ( B e. dom S /\ ( ( # ` B ) - 1 ) e. NN ) -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
46 9 44 45 syl2anc 
 |-  ( ph -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
47 10 46 eqeltrd 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
48 13 fveq2i 
 |-  ( B ` L ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) )
49 48 fveq2i 
 |-  ( T ` ( B ` L ) ) = ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
50 49 rneqi 
 |-  ran ( T ` ( B ` L ) ) = ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
51 47 50 eleqtrrdi 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( B ` L ) ) )
52 1 2 3 4 efgtlen 
 |-  ( ( ( B ` L ) e. W /\ ( S ` A ) e. ran ( T ` ( B ` L ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( B ` L ) ) + 2 ) )
53 28 51 52 syl2anc 
 |-  ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( B ` L ) ) + 2 ) )
54 43 53 eqtr3d 
 |-  ( ph -> ( ( # ` ( A ` K ) ) + 2 ) = ( ( # ` ( B ` L ) ) + 2 ) )
55 27 32 33 54 addcan2ad 
 |-  ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` L ) ) )