Metamath Proof Explorer


Theorem efgredlem

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Hypotheses efgval.w W=IWordI×2𝑜
efgval.r ˙=~FGI
efgval2.m M=yI,z2𝑜y1𝑜z
efgval2.t T=vWn0v,wI×2𝑜vsplicenn⟨“wMw”⟩
efgred.d D=WxWranTx
efgred.s S=mtWordW|t0Dk1..^ttkranTtk1mm1
efgredlem.1 φadomSbdomSSa<SASa=Sba0=b0
efgredlem.2 φAdomS
efgredlem.3 φBdomS
efgredlem.4 φSA=SB
efgredlem.5 φ¬A0=B0
Assertion efgredlem ¬φ

Proof

Step Hyp Ref Expression
1 efgval.w W=IWordI×2𝑜
2 efgval.r ˙=~FGI
3 efgval2.m M=yI,z2𝑜y1𝑜z
4 efgval2.t T=vWn0v,wI×2𝑜vsplicenn⟨“wMw”⟩
5 efgred.d D=WxWranTx
6 efgred.s S=mtWordW|t0Dk1..^ttkranTtk1mm1
7 efgredlem.1 φadomSbdomSSa<SASa=Sba0=b0
8 efgredlem.2 φAdomS
9 efgredlem.3 φBdomS
10 efgredlem.4 φSA=SB
11 efgredlem.5 φ¬A0=B0
12 fviss IWordI×2𝑜WordI×2𝑜
13 1 12 eqsstri WWordI×2𝑜
14 1 2 3 4 5 6 efgsdm AdomSAWordWA0Di1..^AAiranTAi1
15 14 simp1bi AdomSAWordW
16 8 15 syl φAWordW
17 16 eldifad φAWordW
18 wrdf AWordWA:0..^AW
19 17 18 syl φA:0..^AW
20 1 2 3 4 5 6 7 8 9 10 11 efgredlema φA1B1
21 20 simpld φA1
22 nnm1nn0 A1A-1-10
23 21 22 syl φA-1-10
24 21 nnred φA1
25 24 lem1d φA-1-1A1
26 eldifsni AWordWA
27 8 15 26 3syl φA
28 wrdfin AWordWAFin
29 hashnncl AFinAA
30 17 28 29 3syl φAA
31 27 30 mpbird φA
32 nnm1nn0 AA10
33 fznn0 A10A-1-10A1A-1-10A-1-1A1
34 31 32 33 3syl φA-1-10A1A-1-10A-1-1A1
35 23 25 34 mpbir2and φA-1-10A1
36 lencl AWordWA0
37 17 36 syl φA0
38 37 nn0zd φA
39 fzoval A0..^A=0A1
40 38 39 syl φ0..^A=0A1
41 35 40 eleqtrrd φA-1-10..^A
42 19 41 ffvelrnd φAA-1-1W
43 13 42 sselid φAA-1-1WordI×2𝑜
44 lencl AA-1-1WordI×2𝑜AA-1-10
45 43 44 syl φAA-1-10
46 45 nn0red φAA-1-1
47 2rp 2+
48 ltaddrp AA-1-12+AA-1-1<AA-1-1+2
49 46 47 48 sylancl φAA-1-1<AA-1-1+2
50 37 nn0red φA
51 50 lem1d φA1A
52 fznn AA11AA1A1A
53 38 52 syl φA11AA1A1A
54 21 51 53 mpbir2and φA11A
55 1 2 3 4 5 6 efgsres AdomSA11AA0..^A1domS
56 8 54 55 syl2anc φA0..^A1domS
57 1 2 3 4 5 6 efgsval A0..^A1domSSA0..^A1=A0..^A1A0..^A11
58 56 57 syl φSA0..^A1=A0..^A1A0..^A11
59 fz1ssfz0 1A0A
60 59 54 sselid φA10A
61 pfxres AWordWA10AAprefixA1=A0..^A1
62 17 60 61 syl2anc φAprefixA1=A0..^A1
63 62 fveq2d φAprefixA1=A0..^A1
64 pfxlen AWordWA10AAprefixA1=A1
65 17 60 64 syl2anc φAprefixA1=A1
66 63 65 eqtr3d φA0..^A1=A1
67 66 fvoveq1d φA0..^A1A0..^A11=A0..^A1A-1-1
68 fzo0end A1A-1-10..^A1
69 fvres A-1-10..^A1A0..^A1A-1-1=AA-1-1
70 21 68 69 3syl φA0..^A1A-1-1=AA-1-1
71 58 67 70 3eqtrd φSA0..^A1=AA-1-1
72 71 fveq2d φSA0..^A1=AA-1-1
73 1 2 3 4 5 6 efgsdmi AdomSA1SAranTAA-1-1
74 8 21 73 syl2anc φSAranTAA-1-1
75 1 2 3 4 efgtlen AA-1-1WSAranTAA-1-1SA=AA-1-1+2
76 42 74 75 syl2anc φSA=AA-1-1+2
77 49 72 76 3brtr4d φSA0..^A1<SA
78 1 2 3 4 efgtf AA-1-1WTAA-1-1=a0AA-1-1,bI×2𝑜AA-1-1spliceaa⟨“bMb”⟩TAA-1-1:0AA-1-1×I×2𝑜W
79 42 78 syl φTAA-1-1=a0AA-1-1,bI×2𝑜AA-1-1spliceaa⟨“bMb”⟩TAA-1-1:0AA-1-1×I×2𝑜W
80 79 simprd φTAA-1-1:0AA-1-1×I×2𝑜W
81 ffn TAA-1-1:0AA-1-1×I×2𝑜WTAA-1-1Fn0AA-1-1×I×2𝑜
82 ovelrn TAA-1-1Fn0AA-1-1×I×2𝑜SAranTAA-1-1i0AA-1-1rI×2𝑜SA=iTAA-1-1r
83 80 81 82 3syl φSAranTAA-1-1i0AA-1-1rI×2𝑜SA=iTAA-1-1r
84 74 83 mpbid φi0AA-1-1rI×2𝑜SA=iTAA-1-1r
85 20 simprd φB1
86 1 2 3 4 5 6 efgsdmi BdomSB1SBranTBB-1-1
87 9 85 86 syl2anc φSBranTBB-1-1
88 1 2 3 4 5 6 efgsdm BdomSBWordWB0Di1..^BBiranTBi1
89 88 simp1bi BdomSBWordW
90 9 89 syl φBWordW
91 90 eldifad φBWordW
92 wrdf BWordWB:0..^BW
93 91 92 syl φB:0..^BW
94 fzo0end B1B-1-10..^B1
95 elfzofz B-1-10..^B1B-1-10B1
96 85 94 95 3syl φB-1-10B1
97 lencl BWordWB0
98 91 97 syl φB0
99 98 nn0zd φB
100 fzoval B0..^B=0B1
101 99 100 syl φ0..^B=0B1
102 96 101 eleqtrrd φB-1-10..^B
103 93 102 ffvelrnd φBB-1-1W
104 1 2 3 4 efgtf BB-1-1WTBB-1-1=a0BB-1-1,bI×2𝑜BB-1-1spliceaa⟨“bMb”⟩TBB-1-1:0BB-1-1×I×2𝑜W
105 103 104 syl φTBB-1-1=a0BB-1-1,bI×2𝑜BB-1-1spliceaa⟨“bMb”⟩TBB-1-1:0BB-1-1×I×2𝑜W
106 105 simprd φTBB-1-1:0BB-1-1×I×2𝑜W
107 ffn TBB-1-1:0BB-1-1×I×2𝑜WTBB-1-1Fn0BB-1-1×I×2𝑜
108 ovelrn TBB-1-1Fn0BB-1-1×I×2𝑜SBranTBB-1-1j0BB-1-1sI×2𝑜SB=jTBB-1-1s
109 106 107 108 3syl φSBranTBB-1-1j0BB-1-1sI×2𝑜SB=jTBB-1-1s
110 87 109 mpbid φj0BB-1-1sI×2𝑜SB=jTBB-1-1s
111 reeanv i0AA-1-1j0BB-1-1rI×2𝑜SA=iTAA-1-1rsI×2𝑜SB=jTBB-1-1si0AA-1-1rI×2𝑜SA=iTAA-1-1rj0BB-1-1sI×2𝑜SB=jTBB-1-1s
112 reeanv rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1srI×2𝑜SA=iTAA-1-1rsI×2𝑜SB=jTBB-1-1s
113 7 ad3antrrr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1adomSbdomSSa<SASa=Sba0=b0
114 8 ad3antrrr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1AdomS
115 9 ad3antrrr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1BdomS
116 10 ad3antrrr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1SA=SB
117 11 ad3antrrr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1¬A0=B0
118 eqid A-1-1=A-1-1
119 eqid B-1-1=B-1-1
120 simpllr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1i0AA-1-1j0BB-1-1
121 120 simpld φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1i0AA-1-1
122 120 simprd φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1j0BB-1-1
123 simplrl φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1rI×2𝑜sI×2𝑜
124 123 simpld φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1rI×2𝑜
125 123 simprd φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1sI×2𝑜
126 simplrr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1SA=iTAA-1-1rSB=jTBB-1-1s
127 126 simpld φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1SA=iTAA-1-1r
128 126 simprd φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1SB=jTBB-1-1s
129 simpr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1¬AA-1-1=BB-1-1
130 1 2 3 4 5 6 113 114 115 116 117 118 119 121 122 124 125 127 128 129 efgredlemb ¬φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1
131 iman φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1sAA-1-1=BB-1-1¬φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1s¬AA-1-1=BB-1-1
132 130 131 mpbir φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1sAA-1-1=BB-1-1
133 132 expr φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1sAA-1-1=BB-1-1
134 133 rexlimdvva φi0AA-1-1j0BB-1-1rI×2𝑜sI×2𝑜SA=iTAA-1-1rSB=jTBB-1-1sAA-1-1=BB-1-1
135 112 134 syl5bir φi0AA-1-1j0BB-1-1rI×2𝑜SA=iTAA-1-1rsI×2𝑜SB=jTBB-1-1sAA-1-1=BB-1-1
136 135 rexlimdvva φi0AA-1-1j0BB-1-1rI×2𝑜SA=iTAA-1-1rsI×2𝑜SB=jTBB-1-1sAA-1-1=BB-1-1
137 111 136 syl5bir φi0AA-1-1rI×2𝑜SA=iTAA-1-1rj0BB-1-1sI×2𝑜SB=jTBB-1-1sAA-1-1=BB-1-1
138 84 110 137 mp2and φAA-1-1=BB-1-1
139 fvres B-1-10..^B1B0..^B1B-1-1=BB-1-1
140 85 94 139 3syl φB0..^B1B-1-1=BB-1-1
141 138 70 140 3eqtr4d φA0..^A1A-1-1=B0..^B1B-1-1
142 fz1ssfz0 1B0B
143 98 nn0red φB
144 143 lem1d φB1B
145 fznn BB11BB1B1B
146 99 145 syl φB11BB1B1B
147 85 144 146 mpbir2and φB11B
148 142 147 sselid φB10B
149 pfxres BWordWB10BBprefixB1=B0..^B1
150 91 148 149 syl2anc φBprefixB1=B0..^B1
151 150 fveq2d φBprefixB1=B0..^B1
152 pfxlen BWordWB10BBprefixB1=B1
153 91 148 152 syl2anc φBprefixB1=B1
154 151 153 eqtr3d φB0..^B1=B1
155 154 fvoveq1d φB0..^B1B0..^B11=B0..^B1B-1-1
156 141 67 155 3eqtr4d φA0..^A1A0..^A11=B0..^B1B0..^B11
157 1 2 3 4 5 6 efgsres BdomSB11BB0..^B1domS
158 9 147 157 syl2anc φB0..^B1domS
159 1 2 3 4 5 6 efgsval B0..^B1domSSB0..^B1=B0..^B1B0..^B11
160 158 159 syl φSB0..^B1=B0..^B1B0..^B11
161 156 58 160 3eqtr4d φSA0..^A1=SB0..^B1
162 fveq2 a=A0..^A1Sa=SA0..^A1
163 162 fveq2d a=A0..^A1Sa=SA0..^A1
164 163 breq1d a=A0..^A1Sa<SASA0..^A1<SA
165 162 eqeq1d a=A0..^A1Sa=SbSA0..^A1=Sb
166 fveq1 a=A0..^A1a0=A0..^A10
167 166 eqeq1d a=A0..^A1a0=b0A0..^A10=b0
168 165 167 imbi12d a=A0..^A1Sa=Sba0=b0SA0..^A1=SbA0..^A10=b0
169 164 168 imbi12d a=A0..^A1Sa<SASa=Sba0=b0SA0..^A1<SASA0..^A1=SbA0..^A10=b0
170 fveq2 b=B0..^B1Sb=SB0..^B1
171 170 eqeq2d b=B0..^B1SA0..^A1=SbSA0..^A1=SB0..^B1
172 fveq1 b=B0..^B1b0=B0..^B10
173 172 eqeq2d b=B0..^B1A0..^A10=b0A0..^A10=B0..^B10
174 171 173 imbi12d b=B0..^B1SA0..^A1=SbA0..^A10=b0SA0..^A1=SB0..^B1A0..^A10=B0..^B10
175 174 imbi2d b=B0..^B1SA0..^A1<SASA0..^A1=SbA0..^A10=b0SA0..^A1<SASA0..^A1=SB0..^B1A0..^A10=B0..^B10
176 169 175 rspc2va A0..^A1domSB0..^B1domSadomSbdomSSa<SASa=Sba0=b0SA0..^A1<SASA0..^A1=SB0..^B1A0..^A10=B0..^B10
177 56 158 7 176 syl21anc φSA0..^A1<SASA0..^A1=SB0..^B1A0..^A10=B0..^B10
178 77 161 177 mp2d φA0..^A10=B0..^B10
179 lbfzo0 00..^A1A1
180 21 179 sylibr φ00..^A1
181 180 fvresd φA0..^A10=A0
182 lbfzo0 00..^B1B1
183 85 182 sylibr φ00..^B1
184 183 fvresd φB0..^B10=B0
185 178 181 184 3eqtr3d φA0=B0
186 185 11 pm2.65i ¬φ