Metamath Proof Explorer

Theorem efgredeu

Description: There is a unique reduced word equivalent to a given word. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypotheses efgval.w ⊢W=I⁡WordI×2𝑜
efgval.r ⊢∼˙=~FG⁡I
efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
Assertion efgredeu ⊢A∈W→∃!d∈Dd∼˙A

Proof

Step Hyp Ref Expression
1 efgval.w ⊢W=I⁡WordI×2𝑜
2 efgval.r ⊢∼˙=~FG⁡I
3 efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
4 efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
5 efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
6 efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
7 1 2 3 4 5 6 efgsfo ⊢S:dom⁡S⟶ontoW
8 foelrn ⊢S:dom⁡S⟶ontoW∧A∈W→∃a∈dom⁡SA=S⁡a
9 7 8 mpan ⊢A∈W→∃a∈dom⁡SA=S⁡a
10 1 2 3 4 5 6 efgsdm ⊢a∈dom⁡S↔a∈WordW∖∅∧a⁡0∈D∧∀i∈1..^aa⁡i∈ran⁡T⁡a⁡i−1
11 10 simp2bi ⊢a∈dom⁡S→a⁡0∈D
12 1 2 3 4 5 6 efgsrel ⊢a∈dom⁡S→a⁡0∼˙S⁡a
13 12 adantl ⊢A∈W∧a∈dom⁡S→a⁡0∼˙S⁡a
14 breq1 ⊢d=a⁡0→d∼˙S⁡a↔a⁡0∼˙S⁡a
15 14 rspcev ⊢a⁡0∈D∧a⁡0∼˙S⁡a→∃d∈Dd∼˙S⁡a
16 11 13 15 syl2an2 ⊢A∈W∧a∈dom⁡S→∃d∈Dd∼˙S⁡a
17 breq2 ⊢A=S⁡a→d∼˙A↔d∼˙S⁡a
18 17 rexbidv ⊢A=S⁡a→∃d∈Dd∼˙A↔∃d∈Dd∼˙S⁡a
19 16 18 syl5ibrcom ⊢A∈W∧a∈dom⁡S→A=S⁡a→∃d∈Dd∼˙A
20 19 rexlimdva ⊢A∈W→∃a∈dom⁡SA=S⁡a→∃d∈Dd∼˙A
21 9 20 mpd ⊢A∈W→∃d∈Dd∼˙A
22 1 2 efger ⊢∼˙ErW
23 22 a1i ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→∼˙ErW
24 simprl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→d∼˙A
25 simprr ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→c∼˙A
26 23 24 25 ertr4d ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→d∼˙c
27 1 2 3 4 5 6 efgrelex ⊢d∼˙c→∃a∈S-1d∃b∈S-1ca⁡0=b⁡0
28 fofn ⊢S:dom⁡S⟶ontoW→SFndom⁡S
29 fniniseg ⊢SFndom⁡S→a∈S-1d↔a∈dom⁡S∧S⁡a=d
30 7 28 29 mp2b ⊢a∈S-1d↔a∈dom⁡S∧S⁡a=d
31 30 simplbi ⊢a∈S-1d→a∈dom⁡S
32 31 ad2antrl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a∈dom⁡S
33 1 2 3 4 5 6 efgsval ⊢a∈dom⁡S→S⁡a=a⁡a−1
34 32 33 syl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡a=a⁡a−1
35 30 simprbi ⊢a∈S-1d→S⁡a=d
36 35 ad2antrl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡a=d
37 simpllr ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→d∈D∧c∈D
38 37 simpld ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→d∈D
39 36 38 eqeltrd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡a∈D
40 1 2 3 4 5 6 efgs1b ⊢a∈dom⁡S→S⁡a∈D↔a=1
41 32 40 syl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡a∈D↔a=1
42 39 41 mpbid ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a=1
43 42 oveq1d ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a−1=1−1
44 1m1e0 ⊢1−1=0
45 43 44 eqtrdi ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a−1=0
46 45 fveq2d ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a⁡a−1=a⁡0
47 34 36 46 3eqtr3rd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a⁡0=d
48 fniniseg ⊢SFndom⁡S→b∈S-1c↔b∈dom⁡S∧S⁡b=c
49 7 28 48 mp2b ⊢b∈S-1c↔b∈dom⁡S∧S⁡b=c
50 49 simplbi ⊢b∈S-1c→b∈dom⁡S
51 50 ad2antll ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→b∈dom⁡S
52 1 2 3 4 5 6 efgsval ⊢b∈dom⁡S→S⁡b=b⁡b−1
53 51 52 syl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡b=b⁡b−1
54 49 simprbi ⊢b∈S-1c→S⁡b=c
55 54 ad2antll ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡b=c
56 37 simprd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→c∈D
57 55 56 eqeltrd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡b∈D
58 1 2 3 4 5 6 efgs1b ⊢b∈dom⁡S→S⁡b∈D↔b=1
59 51 58 syl ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→S⁡b∈D↔b=1
60 57 59 mpbid ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→b=1
61 60 oveq1d ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→b−1=1−1
62 61 44 eqtrdi ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→b−1=0
63 62 fveq2d ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→b⁡b−1=b⁡0
64 53 55 63 3eqtr3rd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→b⁡0=c
65 47 64 eqeq12d ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a⁡0=b⁡0↔d=c
66 65 biimpd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A∧a∈S-1d∧b∈S-1c→a⁡0=b⁡0→d=c
67 66 rexlimdvva ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→∃a∈S-1d∃b∈S-1ca⁡0=b⁡0→d=c
68 27 67 syl5 ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→d∼˙c→d=c
69 26 68 mpd ⊢A∈W∧d∈D∧c∈D∧d∼˙A∧c∼˙A→d=c
70 69 ex ⊢A∈W∧d∈D∧c∈D→d∼˙A∧c∼˙A→d=c
71 70 ralrimivva ⊢A∈W→∀d∈D∀c∈Dd∼˙A∧c∼˙A→d=c
72 breq1 ⊢d=c→d∼˙A↔c∼˙A
73 72 reu4 ⊢∃!d∈Dd∼˙A↔∃d∈Dd∼˙A∧∀d∈D∀c∈Dd∼˙A∧c∼˙A→d=c
74 21 71 73 sylanbrc ⊢A∈W→∃!d∈Dd∼˙A