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 ⁡ 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 efgredeu ⊢ A ∈ W → ∃! d ∈ D d ∼ ˙ A

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 efgsfo ⊢ S : dom ⁡ S ⟶ onto W
8 foelrn ⊢ S : dom ⁡ S ⟶ onto W ∧ A ∈ W → ∃ a ∈ dom ⁡ S A = S ⁡ a
9 7 8 mpan ⊢ A ∈ W → ∃ a ∈ dom ⁡ S A = S ⁡ a
10 1 2 3 4 5 6 efgsdm ⊢ a ∈ dom ⁡ S ↔ a ∈ Word W ∖ ∅ ∧ a ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ a a ⁡ 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 ∈ D d ∼ ˙ S ⁡ a
16 11 13 15 syl2an2 ⊢ A ∈ W ∧ a ∈ dom ⁡ S → ∃ d ∈ D d ∼ ˙ S ⁡ a
17 breq2 ⊢ A = S ⁡ a → d ∼ ˙ A ↔ d ∼ ˙ S ⁡ a
18 17 rexbidv ⊢ A = S ⁡ a → ∃ d ∈ D d ∼ ˙ A ↔ ∃ d ∈ D d ∼ ˙ S ⁡ a
19 16 18 syl5ibrcom ⊢ A ∈ W ∧ a ∈ dom ⁡ S → A = S ⁡ a → ∃ d ∈ D d ∼ ˙ A
20 19 rexlimdva ⊢ A ∈ W → ∃ a ∈ dom ⁡ S A = S ⁡ a → ∃ d ∈ D d ∼ ˙ A
21 9 20 mpd ⊢ A ∈ W → ∃ d ∈ D d ∼ ˙ A
22 1 2 efger ⊢ ∼ ˙ Er W
23 22 a1i ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A → ∼ ˙ Er W
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 -1 d ∃ b ∈ S -1 c a ⁡ 0 = b ⁡ 0
28 fofn ⊢ S : dom ⁡ S ⟶ onto W → S Fn dom ⁡ S
29 fniniseg ⊢ S Fn dom ⁡ S → a ∈ S -1 d ↔ a ∈ dom ⁡ S ∧ S ⁡ a = d
30 7 28 29 mp2b ⊢ a ∈ S -1 d ↔ a ∈ dom ⁡ S ∧ S ⁡ a = d
31 30 simplbi ⊢ a ∈ S -1 d → a ∈ dom ⁡ S
32 31 ad2antrl ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → 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 -1 d ∧ b ∈ S -1 c → S ⁡ a = a ⁡ a − 1
35 30 simprbi ⊢ a ∈ S -1 d → S ⁡ a = d
36 35 ad2antrl ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → S ⁡ a = d
37 simpllr ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → d ∈ D ∧ c ∈ D
38 37 simpld ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → d ∈ D
39 36 38 eqeltrd ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → 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 -1 d ∧ b ∈ S -1 c → S ⁡ a ∈ D ↔ a = 1
42 39 41 mpbid ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → a = 1
43 42 oveq1d ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → 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 -1 d ∧ b ∈ S -1 c → a − 1 = 0
46 45 fveq2d ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → a ⁡ a − 1 = a ⁡ 0
47 34 36 46 3eqtr3rd ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → a ⁡ 0 = d
48 fniniseg ⊢ S Fn dom ⁡ S → b ∈ S -1 c ↔ b ∈ dom ⁡ S ∧ S ⁡ b = c
49 7 28 48 mp2b ⊢ b ∈ S -1 c ↔ b ∈ dom ⁡ S ∧ S ⁡ b = c
50 49 simplbi ⊢ b ∈ S -1 c → b ∈ dom ⁡ S
51 50 ad2antll ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → 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 -1 d ∧ b ∈ S -1 c → S ⁡ b = b ⁡ b − 1
54 49 simprbi ⊢ b ∈ S -1 c → S ⁡ b = c
55 54 ad2antll ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → S ⁡ b = c
56 37 simprd ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → c ∈ D
57 55 56 eqeltrd ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → 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 -1 d ∧ b ∈ S -1 c → S ⁡ b ∈ D ↔ b = 1
60 57 59 mpbid ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → b = 1
61 60 oveq1d ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → b − 1 = 1 − 1
62 61 44 eqtrdi ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → b − 1 = 0
63 62 fveq2d ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → b ⁡ b − 1 = b ⁡ 0
64 53 55 63 3eqtr3rd ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → b ⁡ 0 = c
65 47 64 eqeq12d ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → a ⁡ 0 = b ⁡ 0 ↔ d = c
66 65 biimpd ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A ∧ a ∈ S -1 d ∧ b ∈ S -1 c → a ⁡ 0 = b ⁡ 0 → d = c
67 66 rexlimdvva ⊢ A ∈ W ∧ d ∈ D ∧ c ∈ D ∧ d ∼ ˙ A ∧ c ∼ ˙ A → ∃ a ∈ S -1 d ∃ b ∈ S -1 c a ⁡ 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 ∈ D d ∼ ˙ A ∧ c ∼ ˙ A → d = c
72 breq1 ⊢ d = c → d ∼ ˙ A ↔ c ∼ ˙ A
73 72 reu4 ⊢ ∃! d ∈ D d ∼ ˙ A ↔ ∃ d ∈ D d ∼ ˙ A ∧ ∀ d ∈ D ∀ c ∈ D d ∼ ˙ A ∧ c ∼ ˙ A → d = c
74 21 71 73 sylanbrc ⊢ A ∈ W → ∃! d ∈ D d ∼ ˙ A