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 × 2 𝑜
efgval.r ˙ = ~ FG I
efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
efgred.d D = W x W ran T x
efgred.s S = m t Word W | t 0 D k 1 ..^ t t k ran T t k 1 m m 1
Assertion efgsrel F dom S F 0 ˙ S F

Proof

Step Hyp Ref Expression
1 efgval.w W = I Word I × 2 𝑜
2 efgval.r ˙ = ~ FG I
3 efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
4 efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
5 efgred.d D = W x W ran T x
6 efgred.s S = m t Word W | t 0 D k 1 ..^ t t k ran T t k 1 m m 1
7 1 2 3 4 5 6 efgsdm F dom S F Word W F 0 D a 1 ..^ F F a ran T F a 1
8 7 simp1bi F dom S F Word W
9 eldifsn F Word W F Word W F
10 lennncl F Word W F F
11 9 10 sylbi F Word W F
12 fzo0end F F 1 0 ..^ F
13 8 11 12 3syl F dom S F 1 0 ..^ F
14 nnm1nn0 F F 1 0
15 8 11 14 3syl F dom S F 1 0
16 eleq1 a = 0 a 0 ..^ F 0 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 0 ..^ F F 0 ˙ F a 0 0 ..^ F F 0 ˙ F 0
20 19 imbi2d a = 0 F dom S a 0 ..^ F F 0 ˙ F a F dom S 0 0 ..^ F F 0 ˙ F 0
21 eleq1 a = i a 0 ..^ F i 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 0 ..^ F F 0 ˙ F a i 0 ..^ F F 0 ˙ F i
25 24 imbi2d a = i F dom S a 0 ..^ F F 0 ˙ F a F dom S i 0 ..^ F F 0 ˙ F i
26 eleq1 a = i + 1 a 0 ..^ F i + 1 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 0 ..^ F F 0 ˙ F a i + 1 0 ..^ F F 0 ˙ F i + 1
30 29 imbi2d a = i + 1 F dom S a 0 ..^ F F 0 ˙ F a F dom S i + 1 0 ..^ F F 0 ˙ F i + 1
31 eleq1 a = F 1 a 0 ..^ F F 1 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 0 ..^ F F 0 ˙ F a F 1 0 ..^ F F 0 ˙ F F 1
35 34 imbi2d a = F 1 F dom S a 0 ..^ F F 0 ˙ F a F dom S F 1 0 ..^ F F 0 ˙ F F 1
36 1 2 efger ˙ Er W
37 36 a1i F dom S 0 0 ..^ F ˙ Er W
38 eldifi F Word W F Word W
39 wrdf F Word W F : 0 ..^ F W
40 8 38 39 3syl F dom S F : 0 ..^ F W
41 40 ffvelrnda F dom S 0 0 ..^ F F 0 W
42 37 41 erref F dom S 0 0 ..^ F F 0 ˙ F 0
43 42 ex F dom S 0 0 ..^ F F 0 ˙ F 0
44 elnn0uz i 0 i 0
45 peano2fzor i 0 i + 1 0 ..^ F i 0 ..^ F
46 44 45 sylanb i 0 i + 1 0 ..^ F i 0 ..^ F
47 46 3adant1 F dom S i 0 i + 1 0 ..^ F i 0 ..^ F
48 47 3expia F dom S i 0 i + 1 0 ..^ F i 0 ..^ F
49 48 imim1d F dom S i 0 i 0 ..^ F F 0 ˙ F i i + 1 0 ..^ F F 0 ˙ F i
50 40 3ad2ant1 F dom S i 0 i + 1 0 ..^ F F : 0 ..^ F W
51 50 47 ffvelrnd F dom S i 0 i + 1 0 ..^ F F i 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 ran T F a 1 F i + 1 ran T F i + 1 - 1
56 7 simp3bi F dom S a 1 ..^ F F a ran T F a 1
57 56 3ad2ant1 F dom S i 0 i + 1 0 ..^ F a 1 ..^ F F a ran T F a 1
58 nn0p1nn i 0 i + 1
59 58 3ad2ant2 F dom S i 0 i + 1 0 ..^ F i + 1
60 nnuz = 1
61 59 60 eleqtrdi F dom S i 0 i + 1 0 ..^ F i + 1 1
62 elfzolt2b i + 1 0 ..^ F i + 1 i + 1 ..^ F
63 62 3ad2ant3 F dom S i 0 i + 1 0 ..^ F i + 1 i + 1 ..^ F
64 elfzo3 i + 1 1 ..^ F i + 1 1 i + 1 i + 1 ..^ F
65 61 63 64 sylanbrc F dom S i 0 i + 1 0 ..^ F i + 1 1 ..^ F
66 55 57 65 rspcdva F dom S i 0 i + 1 0 ..^ F F i + 1 ran T F i + 1 - 1
67 nn0cn i 0 i
68 67 3ad2ant2 F dom S i 0 i + 1 0 ..^ F i
69 ax-1cn 1
70 pncan i 1 i + 1 - 1 = i
71 68 69 70 sylancl F dom S i 0 i + 1 0 ..^ F i + 1 - 1 = i
72 71 fveq2d F dom S i 0 i + 1 0 ..^ F F i + 1 - 1 = F i
73 72 fveq2d F dom S i 0 i + 1 0 ..^ F T F i + 1 - 1 = T F i
74 73 rneqd F dom S i 0 i + 1 0 ..^ F ran T F i + 1 - 1 = ran T F i
75 66 74 eleqtrd F dom S i 0 i + 1 0 ..^ F F i + 1 ran T F i
76 1 2 3 4 efgi2 F i W F i + 1 ran T F i F i ˙ F i + 1
77 51 75 76 syl2anc F dom S i 0 i + 1 0 ..^ F F i ˙ F i + 1
78 36 a1i F dom S i 0 i + 1 0 ..^ F ˙ Er W
79 78 ertr F dom S i 0 i + 1 0 ..^ F F 0 ˙ F i F i ˙ F i + 1 F 0 ˙ F i + 1
80 77 79 mpan2d F dom S i 0 i + 1 0 ..^ F F 0 ˙ F i F 0 ˙ F i + 1
81 80 3expia F dom S i 0 i + 1 0 ..^ F F 0 ˙ F i F 0 ˙ F i + 1
82 81 a2d F dom S i 0 i + 1 0 ..^ F F 0 ˙ F i i + 1 0 ..^ F F 0 ˙ F i + 1
83 49 82 syld F dom S i 0 i 0 ..^ F F 0 ˙ F i i + 1 0 ..^ F F 0 ˙ F i + 1
84 83 expcom i 0 F dom S i 0 ..^ F F 0 ˙ F i i + 1 0 ..^ F F 0 ˙ F i + 1
85 84 a2d i 0 F dom S i 0 ..^ F F 0 ˙ F i F dom S i + 1 0 ..^ F F 0 ˙ F i + 1
86 20 25 30 35 43 85 nn0ind F 1 0 F dom S F 1 0 ..^ F F 0 ˙ F F 1
87 15 86 mpcom F dom S F 1 0 ..^ F F 0 ˙ F F 1
88 13 87 mpd F dom S F 0 ˙ F F 1
89 1 2 3 4 5 6 efgsval F dom S S F = F F 1
90 88 89 breqtrrd F dom S F 0 ˙ S F