Metamath Proof Explorer

Theorem efgsrel

Description: The start and end of any extension sequence are related (i.e. evaluate to the same element of the quotient group to be created). (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 efgsrel 
|- ( F e. dom S -> ( F ` 0 ) .~ ( S ` F ) )

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 efgsdm 
 |-  ( F e. dom S <-> ( F e. ( Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. a e. ( 1 ..^ ( # ` F ) ) ( F ` a ) e. ran ( T ` ( F ` ( a - 1 ) ) ) ) )
8 7 simp1bi 
 |-  ( F e. dom S -> F e. ( Word W \ { (/) } ) )
9 eldifsn 
 |-  ( F e. ( Word W \ { (/) } ) <-> ( F e. Word W /\ F =/= (/) ) )
10 lennncl 
 |-  ( ( F e. Word W /\ F =/= (/) ) -> ( # ` F ) e. NN )
11 9 10 sylbi 
 |-  ( F e. ( Word W \ { (/) } ) -> ( # ` F ) e. NN )
12 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
13 8 11 12 3syl 
 |-  ( F e. dom S -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
14 nnm1nn0 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. NN0 )
15 8 11 14 3syl 
 |-  ( F e. dom S -> ( ( # ` F ) - 1 ) e. NN0 )
16 eleq1 
 |-  ( a = 0 -> ( a e. ( 0 ..^ ( # ` F ) ) <-> 0 e. ( 0 ..^ ( # ` F ) ) ) )
17 fveq2 
 |-  ( a = 0 -> ( F ` a ) = ( F ` 0 ) )
18 17 breq2d 
 |-  ( a = 0 -> ( ( F ` 0 ) .~ ( F ` a ) <-> ( F ` 0 ) .~ ( F ` 0 ) ) )
19 16 18 imbi12d 
 |-  ( a = 0 -> ( ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) <-> ( 0 e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` 0 ) ) ) )
20 19 imbi2d 
 |-  ( a = 0 -> ( ( F e. dom S -> ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) ) <-> ( F e. dom S -> ( 0 e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` 0 ) ) ) ) )
21 eleq1 
 |-  ( a = i -> ( a e. ( 0 ..^ ( # ` F ) ) <-> i e. ( 0 ..^ ( # ` F ) ) ) )
22 fveq2 
 |-  ( a = i -> ( F ` a ) = ( F ` i ) )
23 22 breq2d 
 |-  ( a = i -> ( ( F ` 0 ) .~ ( F ` a ) <-> ( F ` 0 ) .~ ( F ` i ) ) )
24 21 23 imbi12d 
 |-  ( a = i -> ( ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) <-> ( i e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) ) )
25 24 imbi2d 
 |-  ( a = i -> ( ( F e. dom S -> ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) ) <-> ( F e. dom S -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) ) ) )
26 eleq1 
 |-  ( a = ( i + 1 ) -> ( a e. ( 0 ..^ ( # ` F ) ) <-> ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) )
27 fveq2 
 |-  ( a = ( i + 1 ) -> ( F ` a ) = ( F ` ( i + 1 ) ) )
28 27 breq2d 
 |-  ( a = ( i + 1 ) -> ( ( F ` 0 ) .~ ( F ` a ) <-> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) )
29 26 28 imbi12d 
 |-  ( a = ( i + 1 ) -> ( ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) <-> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) )
30 29 imbi2d 
 |-  ( a = ( i + 1 ) -> ( ( F e. dom S -> ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) ) <-> ( F e. dom S -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) ) )
31 eleq1 
 |-  ( a = ( ( # ` F ) - 1 ) -> ( a e. ( 0 ..^ ( # ` F ) ) <-> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) )
32 fveq2 
 |-  ( a = ( ( # ` F ) - 1 ) -> ( F ` a ) = ( F ` ( ( # ` F ) - 1 ) ) )
33 32 breq2d 
 |-  ( a = ( ( # ` F ) - 1 ) -> ( ( F ` 0 ) .~ ( F ` a ) <-> ( F ` 0 ) .~ ( F ` ( ( # ` F ) - 1 ) ) ) )
34 31 33 imbi12d 
 |-  ( a = ( ( # ` F ) - 1 ) -> ( ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) <-> ( ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( ( # ` F ) - 1 ) ) ) ) )
35 34 imbi2d 
 |-  ( a = ( ( # ` F ) - 1 ) -> ( ( F e. dom S -> ( a e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` a ) ) ) <-> ( F e. dom S -> ( ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( ( # ` F ) - 1 ) ) ) ) ) )
36 1 2 efger 
 |-  .~ Er W
37 36 a1i 
 |-  ( ( F e. dom S /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> .~ Er W )
38 eldifi 
 |-  ( F e. ( Word W \ { (/) } ) -> F e. Word W )
39 wrdf 
 |-  ( F e. Word W -> F : ( 0 ..^ ( # ` F ) ) --> W )
40 8 38 39 3syl 
 |-  ( F e. dom S -> F : ( 0 ..^ ( # ` F ) ) --> W )
41 40 ffvelrnda 
 |-  ( ( F e. dom S /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` 0 ) e. W )
42 37 41 erref 
 |-  ( ( F e. dom S /\ 0 e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` 0 ) .~ ( F ` 0 ) )
43 42 ex 
 |-  ( F e. dom S -> ( 0 e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` 0 ) ) )
44 elnn0uz 
 |-  ( i e. NN0 <-> i e. ( ZZ>= ` 0 ) )
45 peano2fzor 
 |-  ( ( i e. ( ZZ>= ` 0 ) /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
46 44 45 sylanb 
 |-  ( ( i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
47 46 3adant1 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
48 47 3expia 
 |-  ( ( F e. dom S /\ i e. NN0 ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> i e. ( 0 ..^ ( # ` F ) ) ) )
49 48 imim1d 
 |-  ( ( F e. dom S /\ i e. NN0 ) -> ( ( i e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) ) )
50 40 3ad2ant1 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> F : ( 0 ..^ ( # ` F ) ) --> W )
51 50 47 ffvelrnd 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) e. W )
52 fvoveq1 
 |-  ( a = ( i + 1 ) -> ( F ` ( a - 1 ) ) = ( F ` ( ( i + 1 ) - 1 ) ) )
53 52 fveq2d 
 |-  ( a = ( i + 1 ) -> ( T ` ( F ` ( a - 1 ) ) ) = ( T ` ( F ` ( ( i + 1 ) - 1 ) ) ) )
54 53 rneqd 
 |-  ( a = ( i + 1 ) -> ran ( T ` ( F ` ( a - 1 ) ) ) = ran ( T ` ( F ` ( ( i + 1 ) - 1 ) ) ) )
55 27 54 eleq12d 
 |-  ( a = ( i + 1 ) -> ( ( F ` a ) e. ran ( T ` ( F ` ( a - 1 ) ) ) <-> ( F ` ( i + 1 ) ) e. ran ( T ` ( F ` ( ( i + 1 ) - 1 ) ) ) ) )
56 7 simp3bi 
 |-  ( F e. dom S -> A. a e. ( 1 ..^ ( # ` F ) ) ( F ` a ) e. ran ( T ` ( F ` ( a - 1 ) ) ) )
57 56 3ad2ant1 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> A. a e. ( 1 ..^ ( # ` F ) ) ( F ` a ) e. ran ( T ` ( F ` ( a - 1 ) ) ) )
58 nn0p1nn 
 |-  ( i e. NN0 -> ( i + 1 ) e. NN )
59 58 3ad2ant2 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( i + 1 ) e. NN )
60 nnuz 
 |-  NN = ( ZZ>= ` 1 )
61 59 60 eleqtrdi 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( i + 1 ) e. ( ZZ>= ` 1 ) )
62 elfzolt2b 
 |-  ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( i + 1 ) e. ( ( i + 1 ) ..^ ( # ` F ) ) )
63 62 3ad2ant3 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( i + 1 ) e. ( ( i + 1 ) ..^ ( # ` F ) ) )
64 elfzo3 
 |-  ( ( i + 1 ) e. ( 1 ..^ ( # ` F ) ) <-> ( ( i + 1 ) e. ( ZZ>= ` 1 ) /\ ( i + 1 ) e. ( ( i + 1 ) ..^ ( # ` F ) ) ) )
65 61 63 64 sylanbrc 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( i + 1 ) e. ( 1 ..^ ( # ` F ) ) )
66 55 57 65 rspcdva 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` ( i + 1 ) ) e. ran ( T ` ( F ` ( ( i + 1 ) - 1 ) ) ) )
67 nn0cn 
 |-  ( i e. NN0 -> i e. CC )
68 67 3ad2ant2 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> i e. CC )
69 ax-1cn 
 |-  1 e. CC
70 pncan 
 |-  ( ( i e. CC /\ 1 e. CC ) -> ( ( i + 1 ) - 1 ) = i )
71 68 69 70 sylancl 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( i + 1 ) - 1 ) = i )
72 71 fveq2d 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` ( ( i + 1 ) - 1 ) ) = ( F ` i ) )
73 72 fveq2d 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( T ` ( F ` ( ( i + 1 ) - 1 ) ) ) = ( T ` ( F ` i ) ) )
74 73 rneqd 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ran ( T ` ( F ` ( ( i + 1 ) - 1 ) ) ) = ran ( T ` ( F ` i ) ) )
75 66 74 eleqtrd 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` ( i + 1 ) ) e. ran ( T ` ( F ` i ) ) )
76 1 2 3 4 efgi2 
 |-  ( ( ( F ` i ) e. W /\ ( F ` ( i + 1 ) ) e. ran ( T ` ( F ` i ) ) ) -> ( F ` i ) .~ ( F ` ( i + 1 ) ) )
77 51 75 76 syl2anc 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) .~ ( F ` ( i + 1 ) ) )
78 36 a1i 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> .~ Er W )
79 78 ertr 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( F ` 0 ) .~ ( F ` i ) /\ ( F ` i ) .~ ( F ` ( i + 1 ) ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) )
80 77 79 mpan2d 
 |-  ( ( F e. dom S /\ i e. NN0 /\ ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ` 0 ) .~ ( F ` i ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) )
81 80 3expia 
 |-  ( ( F e. dom S /\ i e. NN0 ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( ( F ` 0 ) .~ ( F ` i ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) )
82 81 a2d 
 |-  ( ( F e. dom S /\ i e. NN0 ) -> ( ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) )
83 49 82 syld 
 |-  ( ( F e. dom S /\ i e. NN0 ) -> ( ( i e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) )
84 83 expcom 
 |-  ( i e. NN0 -> ( F e. dom S -> ( ( i e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) ) )
85 84 a2d 
 |-  ( i e. NN0 -> ( ( F e. dom S -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` i ) ) ) -> ( F e. dom S -> ( ( i + 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( i + 1 ) ) ) ) ) )
86 20 25 30 35 43 85 nn0ind 
 |-  ( ( ( # ` F ) - 1 ) e. NN0 -> ( F e. dom S -> ( ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( ( # ` F ) - 1 ) ) ) ) )
87 15 86 mpcom 
 |-  ( F e. dom S -> ( ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) -> ( F ` 0 ) .~ ( F ` ( ( # ` F ) - 1 ) ) ) )
88 13 87 mpd 
 |-  ( F e. dom S -> ( F ` 0 ) .~ ( F ` ( ( # ` F ) - 1 ) ) )
89 1 2 3 4 5 6 efgsval 
 |-  ( F e. dom S -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
90 88 89 breqtrrd 
 |-  ( F e. dom S -> ( F ` 0 ) .~ ( S ` F ) )