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 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 efgredeu 
|- ( A e. W -> E! d e. D d .~ A )

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 efgsfo 
 |-  S : dom S -onto-> W
8 foelrn 
 |-  ( ( S : dom S -onto-> W /\ A e. W ) -> E. a e. dom S A = ( S ` a ) )
9 7 8 mpan 
 |-  ( A e. W -> E. a e. dom S A = ( S ` a ) )
10 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 ) ) ) ) )
11 10 simp2bi 
 |-  ( a e. dom S -> ( a ` 0 ) e. D )
12 1 2 3 4 5 6 efgsrel 
 |-  ( a e. dom S -> ( a ` 0 ) .~ ( S ` a ) )
13 12 adantl 
 |-  ( ( A e. W /\ a e. dom S ) -> ( a ` 0 ) .~ ( S ` a ) )
14 breq1 
 |-  ( d = ( a ` 0 ) -> ( d .~ ( S ` a ) <-> ( a ` 0 ) .~ ( S ` a ) ) )
15 14 rspcev 
 |-  ( ( ( a ` 0 ) e. D /\ ( a ` 0 ) .~ ( S ` a ) ) -> E. d e. D d .~ ( S ` a ) )
16 11 13 15 syl2an2 
 |-  ( ( A e. W /\ a e. dom S ) -> E. d e. D d .~ ( S ` a ) )
17 breq2 
 |-  ( A = ( S ` a ) -> ( d .~ A <-> d .~ ( S ` a ) ) )
18 17 rexbidv 
 |-  ( A = ( S ` a ) -> ( E. d e. D d .~ A <-> E. d e. D d .~ ( S ` a ) ) )
19 16 18 syl5ibrcom 
 |-  ( ( A e. W /\ a e. dom S ) -> ( A = ( S ` a ) -> E. d e. D d .~ A ) )
20 19 rexlimdva 
 |-  ( A e. W -> ( E. a e. dom S A = ( S ` a ) -> E. d e. D d .~ A ) )
21 9 20 mpd 
 |-  ( A e. W -> E. d e. D d .~ A )
22 1 2 efger 
 |-  .~ Er W
23 22 a1i 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> .~ Er W )
24 simprl 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> d .~ A )
25 simprr 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> c .~ A )
26 23 24 25 ertr4d 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> d .~ c )
27 1 2 3 4 5 6 efgrelex 
 |-  ( d .~ c -> E. a e. ( `' S " { d } ) E. b e. ( `' S " { c } ) ( a ` 0 ) = ( b ` 0 ) )
28 fofn 
 |-  ( S : dom S -onto-> W -> S Fn dom S )
29 fniniseg 
 |-  ( S Fn dom S -> ( a e. ( `' S " { d } ) <-> ( a e. dom S /\ ( S ` a ) = d ) ) )
30 7 28 29 mp2b 
 |-  ( a e. ( `' S " { d } ) <-> ( a e. dom S /\ ( S ` a ) = d ) )
31 30 simplbi 
 |-  ( a e. ( `' S " { d } ) -> a e. dom S )
32 31 ad2antrl 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> a e. dom S )
33 1 2 3 4 5 6 efgsval 
 |-  ( a e. dom S -> ( S ` a ) = ( a ` ( ( # ` a ) - 1 ) ) )
34 32 33 syl 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( S ` a ) = ( a ` ( ( # ` a ) - 1 ) ) )
35 30 simprbi 
 |-  ( a e. ( `' S " { d } ) -> ( S ` a ) = d )
36 35 ad2antrl 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( S ` a ) = d )
37 simpllr 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( d e. D /\ c e. D ) )
38 37 simpld 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> d e. D )
39 36 38 eqeltrd 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( S ` a ) e. D )
40 1 2 3 4 5 6 efgs1b 
 |-  ( a e. dom S -> ( ( S ` a ) e. D <-> ( # ` a ) = 1 ) )
41 32 40 syl 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( S ` a ) e. D <-> ( # ` a ) = 1 ) )
42 39 41 mpbid 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( # ` a ) = 1 )
43 42 oveq1d 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( # ` a ) - 1 ) = ( 1 - 1 ) )
44 1m1e0 
 |-  ( 1 - 1 ) = 0
45 43 44 eqtrdi 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( # ` a ) - 1 ) = 0 )
46 45 fveq2d 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( a ` ( ( # ` a ) - 1 ) ) = ( a ` 0 ) )
47 34 36 46 3eqtr3rd 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( a ` 0 ) = d )
48 fniniseg 
 |-  ( S Fn dom S -> ( b e. ( `' S " { c } ) <-> ( b e. dom S /\ ( S ` b ) = c ) ) )
49 7 28 48 mp2b 
 |-  ( b e. ( `' S " { c } ) <-> ( b e. dom S /\ ( S ` b ) = c ) )
50 49 simplbi 
 |-  ( b e. ( `' S " { c } ) -> b e. dom S )
51 50 ad2antll 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> b e. dom S )
52 1 2 3 4 5 6 efgsval 
 |-  ( b e. dom S -> ( S ` b ) = ( b ` ( ( # ` b ) - 1 ) ) )
53 51 52 syl 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( S ` b ) = ( b ` ( ( # ` b ) - 1 ) ) )
54 49 simprbi 
 |-  ( b e. ( `' S " { c } ) -> ( S ` b ) = c )
55 54 ad2antll 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( S ` b ) = c )
56 37 simprd 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> c e. D )
57 55 56 eqeltrd 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( S ` b ) e. D )
58 1 2 3 4 5 6 efgs1b 
 |-  ( b e. dom S -> ( ( S ` b ) e. D <-> ( # ` b ) = 1 ) )
59 51 58 syl 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( S ` b ) e. D <-> ( # ` b ) = 1 ) )
60 57 59 mpbid 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( # ` b ) = 1 )
61 60 oveq1d 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( # ` b ) - 1 ) = ( 1 - 1 ) )
62 61 44 eqtrdi 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( # ` b ) - 1 ) = 0 )
63 62 fveq2d 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( b ` ( ( # ` b ) - 1 ) ) = ( b ` 0 ) )
64 53 55 63 3eqtr3rd 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( b ` 0 ) = c )
65 47 64 eqeq12d 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( a ` 0 ) = ( b ` 0 ) <-> d = c ) )
66 65 biimpd 
 |-  ( ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) /\ ( a e. ( `' S " { d } ) /\ b e. ( `' S " { c } ) ) ) -> ( ( a ` 0 ) = ( b ` 0 ) -> d = c ) )
67 66 rexlimdvva 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> ( E. a e. ( `' S " { d } ) E. b e. ( `' S " { c } ) ( a ` 0 ) = ( b ` 0 ) -> d = c ) )
68 27 67 syl5 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> ( d .~ c -> d = c ) )
69 26 68 mpd 
 |-  ( ( ( A e. W /\ ( d e. D /\ c e. D ) ) /\ ( d .~ A /\ c .~ A ) ) -> d = c )
70 69 ex 
 |-  ( ( A e. W /\ ( d e. D /\ c e. D ) ) -> ( ( d .~ A /\ c .~ A ) -> d = c ) )
71 70 ralrimivva 
 |-  ( A e. W -> A. d e. D A. c e. D ( ( d .~ A /\ c .~ A ) -> d = c ) )
72 breq1 
 |-  ( d = c -> ( d .~ A <-> c .~ A ) )
73 72 reu4 
 |-  ( E! d e. D d .~ A <-> ( E. d e. D d .~ A /\ A. d e. D A. c e. D ( ( d .~ A /\ c .~ A ) -> d = c ) ) )
74 21 71 73 sylanbrc 
 |-  ( A e. W -> E! d e. D d .~ A )