MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eupatrl Unicode version

Theorem eupatrl 21726
Description: An Eulerian path is a trail.

Unfortunately, the edge function of an Eulerian path has the domain , whereas the edge functions of all kinds of walks defined here have the domain (i.e. the edge functions are "words of edge indices", see discussion and proposal of Mario Carneiro at https://groups.google.com/d/msg/metamath/KdVXdL3IH3k/2-BYcS_ACQAJ). Therefore, the arguments of the edge function of an Eulerian path must be shifted by 1 to obtain an edge function of a trail in this theorem, using the auxiliary theorems above (fargshiftlem 21657, fargshiftfv 21658, etc.). TODO: The definition of an Eulerian path and all related theorems should be modified to fit to the general definition of a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.)

Hypothesis
Ref Expression
eupatrl.f
Assertion
Ref Expression
eupatrl
Distinct variable groups:   ,   ,   ,P   ,
Allowed substitution hint:   ( )

Proof of Theorem eupatrl
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-eupa 21721 . . . 4
21brovmpt2ex 6529 . . 3
3 eupatrl.f . . . . . . 7
4 ovex 6158 . . . . . . . 8
54mptex 6018 . . . . . . 7
63, 5eqeltri 2517 . . . . . 6
76a1i 11 . . . . 5
87anim1i 553 . . . 4
98anim2i 554 . . 3
102, 9syl 16 . 2
11 f1ofn 5726 . . . . . . . . . . . . 13
12 fseq1hash 11705 . . . . . . . . . . . . 13
1311, 12sylan2 462 . . . . . . . . . . . 12
1413ancoms 441 . . . . . . . . . . 11
15 f1of1 5724 . . . . . . . . . . . . . . . . . 18
163fargshiftf1 21660 . . . . . . . . . . . . . . . . . . 19
1716expcom 426 . . . . . . . . . . . . . . . . . 18
1815, 17syl 16 . . . . . . . . . . . . . . . . 17
1918imp 420 . . . . . . . . . . . . . . . 16
20 f1ofo 5732 . . . . . . . . . . . . . . . . . 18
213fargshiftfo 21661 . . . . . . . . . . . . . . . . . . 19
2221expcom 426 . . . . . . . . . . . . . . . . . 18
2320, 22syl 16 . . . . . . . . . . . . . . . . 17
2423imp 420 . . . . . . . . . . . . . . . 16
25 df-f1o 5512 . . . . . . . . . . . . . . . 16
2619, 24, 25sylanbrc 647 . . . . . . . . . . . . . . 15
27 f1ofn 5726 . . . . . . . . . . . . . . . . 17
28 hashfn 11704 . . . . . . . . . . . . . . . . . . 19
2928anim2i 554 . . . . . . . . . . . . . . . . . 18
3029ancoms 441 . . . . . . . . . . . . . . . . 17
3127, 30sylan 459 . . . . . . . . . . . . . . . 16
32 hashfzo0 11750 . . . . . . . . . . . . . . . . . . 19
3332eqeq2d 2458 . . . . . . . . . . . . . . . . . 18
3433biimpa 472 . . . . . . . . . . . . . . . . 17
35 pm3.2 436 . . . . . . . . . . . . . . . . . 18
3635adantr 453 . . . . . . . . . . . . . . . . 17
3734, 36syl5com 29 . . . . . . . . . . . . . . . 16
3831, 37mpcom 35 . . . . . . . . . . . . . . 15
3926, 38sylancom 650 . . . . . . . . . . . . . 14
40 df-f1 5510 . . . . . . . . . . . . . . . . . . . . 21
41 iswrdi 11786 . . . . . . . . . . . . . . . . . . . . . 22
4241adantr 453 . . . . . . . . . . . . . . . . . . . . 21
4340, 42sylbi 189 . . . . . . . . . . . . . . . . . . . 20
4443adantr 453 . . . . . . . . . . . . . . . . . . 19
4525, 44sylbi 189 . . . . . . . . . . . . . . . . . 18
4645ad4antr 714 . . . . . . . . . . . . . . . . 17
4740simprbi 452 . . . . . . . . . . . . . . . . . . . 20
4847adantr 453 . . . . . . . . . . . . . . . . . . 19
4925, 48sylbi 189 . . . . . . . . . . . . . . . . . 18
5049ad4antr 714 . . . . . . . . . . . . . . . . 17
5146, 50jca 520 . . . . . . . . . . . . . . . 16
52 eqcom 2449 . . . . . . . . . . . . . . . . . . . . 21
5352biimpi 188 . . . . . . . . . . . . . . . . . . . 20
5453ad3antlr 713 . . . . . . . . . . . . . . . . . . 19
5554oveq2d 6149 . . . . . . . . . . . . . . . . . 18
5655feq2d 5632 . . . . . . . . . . . . . . . . 17
5756biimpa 472 . . . . . . . . . . . . . . . 16
58 f1of 5725 . . . . . . . . . . . . . . . . . . . . . 22
59 fargshiftlem 21657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60 simpll 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
61 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
6261fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
6362adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
64 oveq1 6140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
65 elfzoelz 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
6665zcnd 10431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6766adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
68 ax-1cn 9103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
6968a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
7067, 69pncand 9467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
7164, 70sylan9eqr 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7271fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
73 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
7473adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
7572, 74preq12d 3923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
7663, 75eqeq12d 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
7776ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7877adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7978adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
8079imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
81 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
8281anim1i 553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8382adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
84 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8584ad3antlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
863fargshiftfv 21658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
8786imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8887eqcomd 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
8983, 85, 88syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9089fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9190eqeq1d 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9280, 91bitrd 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9360, 92rspcdv 3068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9493ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9594com23 75 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9659, 95mpancom 652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9796ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9897com24 84 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9998imp31 423 . . . . . . . . . . . . . . . . . . . . . . . . 25
10099ralrimiv 2799 . . . . . . . . . . . . . . . . . . . . . . . 24
101100ex 425 . . . . . . . . . . . . . . . . . . . . . . 23
102101expcom 426 . . . . . . . . . . . . . . . . . . . . . 22
10358, 102syl 16 . . . . . . . . . . . . . . . . . . . . 21
104103imp 420 . . . . . . . . . . . . . . . . . . . 20
105 oveq2 6141 . . . . . . . . . . . . . . . . . . . . . 22
106105raleqdv 2921 . . . . . . . . . . . . . . . . . . . . 21
107106imbi2d 309 . . . . . . . . . . . . . . . . . . . 20
108104, 107syl5ibr 214 . . . . . . . . . . . . . . . . . . 19
109108adantl 454 . . . . . . . . . . . . . . . . . 18
110109imp31 423 . . . . . . . . . . . . . . . . 17
111110adantr 453 . . . . . . . . . . . . . . . 16
11251, 57, 1113jca 1135 . . . . . . . . . . . . . . 15
113112exp31 589 . . . . . . . . . . . . . 14
11439, 113mpancom 652 . . . . . . . . . . . . 13
115114a1i 11 . . . . . . . . . . . 12
116 oveq2 6141 . . . . . . . . . . . . . . 15
117116eqcoms 2450 . . . . . . . . . . . . . 14
118 f1oeq2 5717 . . . . . . . . . . . . . 14
119117, 118syl 16 . . . . . . . . . . . . 13
120 eleq1 2507 . . . . . . . . . . . . . 14
121120eqcoms 2450 . . . . . . . . . . . . 13
122119, 121anbi12d 693 . . . . . . . . . . . 12
123117raleqdv 2921 . . . . . . . . . . . . 13
124 oveq2 6141 . . . . . . . . . . . . . . . 16
125124eqcoms 2450 . . . . . . . . . . . . . . 15
126125feq2d 5632 . . . . . . . . . . . . . 14
127126imbi1d 310 . . . . . . . . . . . . 13
128123, 127imbi12d 313 . . . . . . . . . . . 12