Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  psgnunilem2 Unicode version

Theorem psgnunilem2 27418
 Description: Lemma for psgnuni 27422. Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
Hypotheses
Ref Expression
psgnunilem2.g
psgnunilem2.t pmTrsp
psgnunilem2.d
psgnunilem2.w Word
psgnunilem2.id g
psgnunilem2.l
psgnunilem2.ix ..^
psgnunilem2.a
psgnunilem2.al ..^
psgnunilem2.in Word g
Assertion
Ref Expression
psgnunilem2 Word g ..^ ..^
Distinct variable groups:   ,,,   ,,,   ,   ,   ,,,   ,,,,   ,,,   ,,,,   ,,
Allowed substitution hints:   (,,)   ()   ()   ()   (,)   (,,,)

Proof of Theorem psgnunilem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 psgnunilem2.w . . . . . . . 8 Word
2 wrd0 11418 . . . . . . . 8 Word
3 splcl 11467 . . . . . . . 8 Word Word splice Word
41, 2, 3sylancl 643 . . . . . . 7 splice Word
54adantr 451 . . . . . 6 splice Word
6 fzossfz 10892 . . . . . . . . . . . 12 ..^
7 psgnunilem2.ix . . . . . . . . . . . 12 ..^
86, 7sseldi 3178 . . . . . . . . . . 11
9 elfznn0 10822 . . . . . . . . . . 11
108, 9syl 15 . . . . . . . . . 10
11 2nn0 9982 . . . . . . . . . . 11
12 nn0addcl 9999 . . . . . . . . . . 11
1310, 11, 12sylancl 643 . . . . . . . . . 10
1410nn0red 10019 . . . . . . . . . . 11
15 nn0addge1 10010 . . . . . . . . . . 11
1614, 11, 15sylancl 643 . . . . . . . . . 10
17 elfz2nn0 10821 . . . . . . . . . 10
1810, 13, 16, 17syl3anbrc 1136 . . . . . . . . 9
1910nn0cnd 10020 . . . . . . . . . . . . 13
20 ax-1cn 8795 . . . . . . . . . . . . . 14
2120a1i 10 . . . . . . . . . . . . 13
2219, 21, 21addassd 8857 . . . . . . . . . . . 12
23 df-2 9804 . . . . . . . . . . . . 13
2423oveq2i 5869 . . . . . . . . . . . 12
2522, 24syl6reqr 2334 . . . . . . . . . . 11
26 psgnunilem2.g . . . . . . . . . . . . 13
27 psgnunilem2.t . . . . . . . . . . . . 13 pmTrsp
28 psgnunilem2.d . . . . . . . . . . . . 13
29 psgnunilem2.id . . . . . . . . . . . . 13 g
30 psgnunilem2.l . . . . . . . . . . . . 13
31 psgnunilem2.a . . . . . . . . . . . . 13
32 psgnunilem2.al . . . . . . . . . . . . 13 ..^
3326, 27, 28, 1, 29, 30, 7, 31, 32psgnunilem5 27417 . . . . . . . . . . . 12 ..^
34 fzofzp1 10916 . . . . . . . . . . . 12 ..^
3533, 34syl 15 . . . . . . . . . . 11
3625, 35eqeltrd 2357 . . . . . . . . . 10
3730oveq2d 5874 . . . . . . . . . 10
3836, 37eleqtrrd 2360 . . . . . . . . 9
392a1i 10 . . . . . . . . 9 Word
401, 18, 38, 39spllen 11469 . . . . . . . 8 splice
41 hash0 11355 . . . . . . . . . . . 12
4241oveq1i 5868 . . . . . . . . . . 11
43 df-neg 9040 . . . . . . . . . . 11
4442, 43eqtr4i 2306 . . . . . . . . . 10
45 2cn 9816 . . . . . . . . . . . 12
46 pncan2 9058 . . . . . . . . . . . 12
4719, 45, 46sylancl 643 . . . . . . . . . . 11
4847negeqd 9046 . . . . . . . . . 10
4944, 48syl5eq 2327 . . . . . . . . 9
5030, 49oveq12d 5876 . . . . . . . 8
51 elfzel2 10796 . . . . . . . . . . 11
528, 51syl 15 . . . . . . . . . 10
5352zcnd 10118 . . . . . . . . 9
54 negsub 9095 . . . . . . . . 9
5553, 45, 54sylancl 643 . . . . . . . 8
5640, 50, 553eqtrd 2319 . . . . . . 7 splice
5756adantr 451 . . . . . 6 splice
58 splid 11468 . . . . . . . . . 10 Word splice substr
591, 18, 38, 58syl12anc 1180 . . . . . . . . 9 splice substr
6059oveq2d 5874 . . . . . . . 8 g splice substr g
6160adantr 451 . . . . . . 7 g splice substr g
62 eqid 2283 . . . . . . . 8
6326symggrp 14780 . . . . . . . . . . 11
6428, 63syl 15 . . . . . . . . . 10
65 grpmnd 14494 . . . . . . . . . 10
6664, 65syl 15 . . . . . . . . 9
6766adantr 451 . . . . . . . 8
6827, 26, 62symgtrf 27410 . . . . . . . . . . 11
69 sswrd 11423 . . . . . . . . . . 11 Word Word
7068, 69ax-mp 8 . . . . . . . . . 10 Word Word
7170, 1sseldi 3178 . . . . . . . . 9 Word
7271adantr 451 . . . . . . . 8 Word
7318adantr 451 . . . . . . . 8
7438adantr 451 . . . . . . . 8
75 swrdcl 11452 . . . . . . . . . 10 Word substr Word
7671, 75syl 15 . . . . . . . . 9 substr Word
7776adantr 451 . . . . . . . 8 substr Word
78 wrd0 11418 . . . . . . . . 9 Word
7978a1i 10 . . . . . . . 8 Word
8030oveq2d 5874 . . . . . . . . . . . . . 14 ..^ ..^
8133, 80eleqtrrd 2360 . . . . . . . . . . . . 13 ..^
82 swrds2 11560 . . . . . . . . . . . . 13 Word ..^ substr
831, 10, 81, 82syl3anc 1182 . . . . . . . . . . . 12 substr
8483oveq2d 5874 . . . . . . . . . . 11 g substr g
85 wrdf 11419 . . . . . . . . . . . . . . . 16 Word ..^
861, 85syl 15 . . . . . . . . . . . . . . 15 ..^
8780feq2d 5380 . . . . . . . . . . . . . . 15 ..^ ..^
8886, 87mpbid 201 . . . . . . . . . . . . . 14 ..^
89 ffvelrn 5663 . . . . . . . . . . . . . 14 ..^ ..^
9088, 7, 89syl2anc 642 . . . . . . . . . . . . 13
9168, 90sseldi 3178 . . . . . . . . . . . 12
92 ffvelrn 5663 . . . . . . . . . . . . . 14 ..^ ..^
9388, 33, 92syl2anc 642 . . . . . . . . . . . . 13
9468, 93sseldi 3178 . . . . . . . . . . . 12
95 eqid 2283 . . . . . . . . . . . . 13
9662, 95gsumws2 14465 . . . . . . . . . . . 12 g
9766, 91, 94, 96syl3anc 1182 . . . . . . . . . . 11 g
9826, 62, 95symgov 14777 . . . . . . . . . . . 12
9991, 94, 98syl2anc 642 . . . . . . . . . . 11
10084, 97, 993eqtrd 2319 . . . . . . . . . 10 g substr
101100adantr 451 . . . . . . . . 9 g substr
102 simpr 447 . . . . . . . . 9
10326symgid 14781 . . . . . . . . . . . 12
10428, 103syl 15 . . . . . . . . . . 11
105 eqid 2283 . . . . . . . . . . . 12
106105gsum0 14457 . . . . . . . . . . 11 g
107104, 106syl6eqr 2333 . . . . . . . . . 10 g
108107adantr 451 . . . . . . . . 9 g
109101, 102, 1083eqtrd 2319 . . . . . . . 8 g substr g
11062, 67, 72, 73, 74, 77, 79, 109gsumspl 14466 . . . . . . 7 g splice substr g splice
11129adantr 451 . . . . . . 7 g
11261, 110, 1113eqtr3d 2323 . . . . . 6 g splice
113 fveq2 5525 . . . . . . . . 9 splice splice
114113eqeq1d 2291 . . . . . . . 8 splice splice
115 oveq2 5866 . . . . . . . . 9 splice g g splice
116115eqeq1d 2291 . . . . . . . 8 splice g g splice
117114, 116anbi12d 691 . . . . . . 7 splice g splice g splice
118117rspcev 2884 . . . . . 6 splice Word splice g splice Word g
1195, 57, 112, 118syl12anc 1180 . . . . 5 Word g
120 psgnunilem2.in . . . . . 6 Word g
121120adantr 451 . . . . 5 Word g
122119, 121pm2.65i 165 . . . 4
123122pm2.21i 123 . . 3 Word g ..^ ..^
124123ex 423 . 2 Word g ..^ ..^
1251adantr 451 . . . . . . 7 Word
126 simprl 732 . . . . . . . 8
127 simprr 733 . . . . . . . 8
128126, 127s2cld 11519 . . . . . . 7 Word
129 splcl 11467 . . . . . . 7 Word Word splice Word
130125, 128, 129syl2anc 642 . . . . . 6 splice Word
131130adantrr 697 . . . . 5 splice Word
13266adantr 451 . . . . . . . 8
13371adantr 451 . . . . . . . 8 Word
13418adantr 451 . . . . . . . 8
13538adantr 451 . . . . . . . 8
13670, 128sseldi 3178 . . . . . . . . 9 Word
137136adantrr 697 . . . . . . . 8 Word
13876adantr 451 . . . . . . . 8 substr Word
139 simprr1 1003 . . . . . . . . 9
140100adantr 451 . . . . . . . . 9 g substr
14166adantr 451 . . . . . . . . . . . 12
14268a1i 10 . . . . . . . . . . . . . 14
143142sselda 3180 . . . . . . . . . . . . 13
144143adantrr 697 . . . . . . . . . . . 12
145142sselda 3180 . . . . . . . . . . . . 13
146145adantrl 696 . . . . . . . . . . . 12
14762, 95gsumws2 14465 . . . . . . . . . . . 12 g
148141, 144, 146, 147syl3anc 1182 . . . . . . . . . . 11 g
14926, 62, 95symgov 14777 . . . . . . . . . . . 12
150144, 146, 149syl2anc 642 . . . . . . . . . . 11
151148, 150eqtrd 2315 . . . . . . . . . 10 g
152151adantrr 697 . . . . . . . . 9 g
153139, 140, 1523eqtr4rd 2326 . . . . . . . 8 g g substr
15462, 132, 133, 134, 135, 137, 138, 153gsumspl 14466 . . . . . . 7 g splice g splice substr
15560adantr 451 . . . . . . 7 g splice substr g
15629adantr 451 . . . . . . 7 g
157154, 155, 1563eqtrd 2319 . . . . . 6 g splice
15818adantr 451 . . . . . . . . 9
15938adantr 451 . . . . . . . . 9
160125, 158, 159, 128spllen 11469 . . . . . . . 8 splice
161 s2len 11537 . . . . . . . . . . . . 13
162161oveq1i 5868 . . . . . . . . . . . 12
16347oveq2d 5874 . . . . . . . . . . . . 13
16445subidi 9117 . . . . . . . . . . . . 13
165163, 164syl6eq 2331 . . . . . . . . . . . 12
166162, 165syl5eq 2327 . . . . . . . . . . 11
167166oveq2d 5874 . . . . . . . . . 10
16830, 53eqeltrd 2357 . . . . . . . . . . 11
169168addid1d 9012 . . . . . . . . . 10
170167, 169, 303eqtrd 2319 . . . . . . . . 9
171170adantr 451 . . . . . . . 8
172160, 171eqtrd 2315 . . . . . . 7 splice
173172adantrr 697 . . . . . 6 splice
174157, 173jca 518 . . . . 5 g splice splice
17533adantr 451 . . . . . 6 ..^
176 simprr2 1004 . . . . . . 7
177 1nn0 9981 . . . . . . . . . . . . . . 15
178 2nn 9877 . . . . . . . . . . . . . . 15
179 1lt2 9886 . . . . . . . . . . . . . . 15
180 elfzo0 10904 . . . . . . . . . . . . . . 15 ..^
181177, 178, 179, 180mpbir3an 1134 . . . . . . . . . . . . . 14 ..^
182161oveq2i 5869 . . . . . . . . . . . . . 14 ..^ ..^
183181, 182eleqtrri 2356 . . . . . . . . . . . . 13 ..^
184183a1i 10 . . . . . . . . . . . 12 ..^
185125, 158, 159, 128, 184splfv2a 11471 . . . . . . . . . . 11 splice
186 s2fv1 11536 . . . . . . . . . . . 12
187186ad2antll 709 . . . . . . . . . . 11
188185, 187eqtrd 2315 . . . . . . . . . 10 splice
189188adantrr 697 . . . . . . . . 9 splice
190189difeq1d 3293 . . . . . . . 8 splice
191190dmeqd 4881 . . . . . . 7 splice
192176, 191eleqtrrd 2360 . . . . . 6 splice
193 fzosplitsni 10921 . . . . . . . . . . 11 ..^ ..^
194 nn0uz 10262 . . . . . . . . . . 11
195193, 194eleq2s 2375 . . . . . . . . . 10 ..^ ..^
19610, 195syl 15 . . . . . . . . 9 ..^ ..^
197196adantr 451 . . . . . . . 8 ..^ ..^
198 fveq2 5525 . . . . . . . . . . . . . . . . . . 19
199198difeq1d 3293 . . . . . . . . . . . . . . . . . 18
200199dmeqd 4881 . . . . . . . . . . . . . . . . 17
201200eleq2d 2350 . . . . . . . . . . . . . . . 16
202201notbid 285 . . . . . . . . . . . . . . 15
203202rspccva 2883 . . . . . . . . . . . . . 14 ..^ ..^
20432, 203sylan 457 . . . . . . . . . . . . 13 ..^
205204adantlr 695 . . . . . . . . . . . 12 ..^
2061ad2antrr 706 . . . . . . . . . . . . . . . 16 ..^ Word
20718ad2antrr 706 . . . . . . . . . . . . . . . 16 ..^
20838ad2antrr 706 . . . . . . . . . . . . . . . 16 ..^
209128adantr 451 . . . . . . . . . . . . . . . 16 ..^ Word
210 simpr 447 . . . . . . . . . . . . . . . 16 ..^ ..^
211206, 207, 208, 209, 210splfv1 11470 . . . . . . . . . . . . . . 15 ..^ splice
212211difeq1d 3293 . . . . . . . . . . . . . 14 ..^ splice
213212dmeqd 4881 . . . . . . . . . . . . 13 ..^ splice
214213eleq2d 2350 . . . . . . . . . . . 12 ..^ splice
215205, 214mtbird 292 . . . . . . . . . . 11 ..^ splice
216215ex 423 . . . . . . . . . 10 ..^ splice
217216adantrr 697 . . . . . . . . 9 ..^ splice
218 simprr3 1005 . . . . . . . . . . 11
219 0nn0 9980 . . . . . . . . . . . . . . . . . . . 20
220 2pos 9828 . . . . . . . . . . . . . . . . . . . 20
221 elfzo0 10904 . . . . . . . . . . . . . . . . . . . 20 ..^
222219, 178, 220, 221mpbir3an 1134 . . . . . . . . . . . . . . . . . . 19 ..^
223222, 182eleqtrri 2356 . . . . . . . . . . . . . . . . . 18 ..^
224223a1i 10 . . . . . . . . . . . . . . . . 17 ..^
225125, 158, 159, 128, 224splfv2a 11471 . . . . . . . . . . . . . . . 16 splice
22619addid1d 9012 . . . . . . . . . . . . . . . . . 18
227226adantr 451 . . . . . . . . . . . . . . . . 17
228227fveq2d 5529 . . . . . . . . . . . . . . . 16 splice splice
229 s2fv0 11535 . . . . . . . . . . . . . . . . 17
230229ad2antrl 708 . . . . . . . . . . . . . . . 16
231225, 228, 2303eqtr3d 2323 . . . . . . . . . . . . . . 15 splice
232231difeq1d 3293 . . . . . . . . . . . . . 14 splice
233232dmeqd 4881 . . . . . . . . . . . . 13 splice
234233eleq2d 2350 . . . . . . . . . . . 12 splice
235234adantrr 697 . . . . . . . . . . 11 splice
236218, 235mtbird 292 . . . . . . . . . 10 splice
237 fveq2 5525 . . . . . . . . . . . . . 14 splice splice
238237difeq1d 3293 . . . . . . . . . . . . 13 splice splice
239238dmeqd 4881 . . . . . . . . . . . 12 splice splice
240239eleq2d 2350 . . . . . . . . . . 11 splice splice
241240notbid 285 . . . . . . . . . 10 splice splice
242236, 241syl5ibrcom 213 . . . . . . . . 9 splice
243217, 242jaod 369 . . . . . . . 8 ..^ splice
244197, 243sylbid 206 . . . . . . 7 ..^ splice
245244ralrimiv 2625 . . . . . 6 ..^ splice
246175, 192, 2453jca 1132 . . . . 5 ..^ splice ..^ splice
247 oveq2 5866 . . . . . . . . 9 splice g g splice
248247eqeq1d 2291 . . . . . . . 8 splice g g splice
249 fveq2 5525 . . . . . . . . 9 splice splice
250249eqeq1d 2291 . . . . . . . 8 splice splice
251248, 250anbi12d 691 . . . . . . 7 splice g g splice splice
252 fveq1 5524 . . . . . . . . . . 11 splice splice
253252difeq1d 3293 . . . . . . . . . 10 splice splice
254253dmeqd 4881 . . . . . . . . 9 splice splice
255254eleq2d 2350 . . . . . . . 8 splice splice
256 fveq1 5524 . . . . . . . . . . . . 13 splice splice
257256difeq1d 3293 . . . . . . . . . . . 12 splice splice
258257dmeqd 4881 . . . . . . . . . . 11 splice splice
259258eleq2d 2350 . . . . . . . . . 10 splice splice
260259notbid 285 . . . . . . . . 9 splice splice
261260ralbidv 2563 . . . . . . . 8 splice ..^ ..^ splice
262255, 2613anbi23d 1255 . . . . . . 7 splice ..^ ..^ ..^ splice ..^ splice
263251, 262anbi12d 691 . . . . . 6 splice g ..^ ..^ g splice splice ..^ splice ..^ splice
264263rspcev 2884 . . . . 5 splice Word g splice splice ..^ splice ..^ splice Word g ..^ ..^
265131, 174, 246, 264syl12anc 1180 . . . 4 Word g ..^ ..^
266265expr 598 . . 3 Word g ..^ ..^
267266rexlimdvva 2674 . 2 Word g ..^ ..^
26827, 28, 90, 93, 31psgnunilem1 27416 . 2
269124, 267, 268mpjaod 370 1 Word g ..^ ..^
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934   wceq 1623   wcel 1684  wral 2543  wrex 2544   cdif 3149   wss 3152  c0 3455  cop 3643  cotp 3644   class class class wbr 4023   cid 4304   cdm 4689   crn 4690   cres 4691   ccom 4693  wf 5251  cfv 5255  (class class class)co 5858  cc 8735  cr 8736  cc0 8737  c1 8738   caddc 8740   clt 8867   cle 8868   cmin 9037  cneg 9038  cn 9746  c2 9795  cn0 9965  cz 10024  cuz 10230  cfz 10782  ..^cfzo 10870  chash 11337  Word cword 11403   substr csubstr 11406   splice csplice 11407  cs2 11491  cbs 13148   cplusg 13208  c0g 13400   g cgsu 13401  cmnd 14361  cgrp 14362  csymg 14769  pmTrspcpmtr 27384 This theorem is referenced by:  psgnunilem3  27419 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-xor 1296  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-ot 3650  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-2o 6480  df-oadd 6483  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-2 9804  df-3 9805  df-4 9806  df-5 9807  df-6 9808  df-7 9809  df-8 9810  df-9 9811  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-fzo 10871  df-seq 11047  df-hash 11338  df-word 11409  df-concat 11410  df-s1 11411  df-substr 11412  df-splice 11413  df-s2 11498  df-struct 13150  df-ndx 13151  df-slot 13152  df-base 13153  df-sets 13154  df-ress 13155  df-plusg 13221  df-tset 13227  df-0g 13404  df-gsum 13405  df-mnd 14367  df-submnd 14416  df-grp 14489  df-minusg 14490  df-subg 14618  df-symg 14770  df-pmtr 27385
 Copyright terms: Public domain W3C validator