Metamath Proof Explorer

Theorem efgredlemf

Description: Lemma for efgredleme . (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 )
Assertion efgredlemf 
|- ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) )

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 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` A ) ) ( A ` i ) e. ran ( T ` ( A ` ( i - 1 ) ) ) ) )
15 14 simp1bi 
 |-  ( A e. dom S -> A e. ( Word W \ { (/) } ) )
16 8 15 syl 
 |-  ( ph -> A e. ( Word W \ { (/) } ) )
17 16 eldifad 
 |-  ( ph -> A e. Word W )
18 wrdf 
 |-  ( A e. Word W -> A : ( 0 ..^ ( # ` A ) ) --> W )
19 17 18 syl 
 |-  ( ph -> A : ( 0 ..^ ( # ` A ) ) --> W )
20 fzossfz 
 |-  ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ... ( ( # ` A ) - 1 ) )
21 lencl 
 |-  ( A e. Word W -> ( # ` A ) e. NN0 )
22 17 21 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
23 22 nn0zd 
 |-  ( ph -> ( # ` A ) e. ZZ )
24 fzoval 
 |-  ( ( # ` A ) e. ZZ -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
25 23 24 syl 
 |-  ( ph -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
26 20 25 sseqtrrid 
 |-  ( ph -> ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ..^ ( # ` A ) ) )
27 1 2 3 4 5 6 7 8 9 10 11 efgredlema 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
28 27 simpld 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. NN )
29 fzo0end 
 |-  ( ( ( # ` A ) - 1 ) e. NN -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
30 28 29 syl 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
31 12 30 eqeltrid 
 |-  ( ph -> K e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
32 26 31 sseldd 
 |-  ( ph -> K e. ( 0 ..^ ( # ` A ) ) )
33 19 32 ffvelrnd 
 |-  ( ph -> ( A ` K ) e. W )
34 1 2 3 4 5 6 efgsdm 
 |-  ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` B ) ) ( B ` i ) e. ran ( T ` ( B ` ( i - 1 ) ) ) ) )
35 34 simp1bi 
 |-  ( B e. dom S -> B e. ( Word W \ { (/) } ) )
36 9 35 syl 
 |-  ( ph -> B e. ( Word W \ { (/) } ) )
37 36 eldifad 
 |-  ( ph -> B e. Word W )
38 wrdf 
 |-  ( B e. Word W -> B : ( 0 ..^ ( # ` B ) ) --> W )
39 37 38 syl 
 |-  ( ph -> B : ( 0 ..^ ( # ` B ) ) --> W )
40 fzossfz 
 |-  ( 0 ..^ ( ( # ` B ) - 1 ) ) C_ ( 0 ... ( ( # ` B ) - 1 ) )
41 lencl 
 |-  ( B e. Word W -> ( # ` B ) e. NN0 )
42 37 41 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
43 42 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
44 fzoval 
 |-  ( ( # ` B ) e. ZZ -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
45 43 44 syl 
 |-  ( ph -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
46 40 45 sseqtrrid 
 |-  ( ph -> ( 0 ..^ ( ( # ` B ) - 1 ) ) C_ ( 0 ..^ ( # ` B ) ) )
47 fzo0end 
 |-  ( ( ( # ` B ) - 1 ) e. NN -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
48 27 47 simpl2im 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
49 13 48 eqeltrid 
 |-  ( ph -> L e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
50 46 49 sseldd 
 |-  ( ph -> L e. ( 0 ..^ ( # ` B ) ) )
51 39 50 ffvelrnd 
 |-  ( ph -> ( B ` L ) e. W )
52 33 51 jca 
 |-  ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) )