Metamath Proof Explorer


Theorem rusgrnumwwlks

Description: Induction step for rusgrnumwwlk . (Contributed by Alexander van der Vekens, 24-Aug-2018) (Revised by AV, 7-May-2021) (Proof shortened by AV, 27-May-2022)

Ref Expression
Hypotheses rusgrnumwwlk.v V = Vtx G
rusgrnumwwlk.l L = v V , n 0 w n WWalksN G | w 0 = v
Assertion rusgrnumwwlks G RegUSGraph K V Fin P V N 0 P L N = K N P L N + 1 = K N + 1

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v V = Vtx G
2 rusgrnumwwlk.l L = v V , n 0 w n WWalksN G | w 0 = v
3 simpr2 G RegUSGraph K V Fin P V N 0 P V
4 simpr3 G RegUSGraph K V Fin P V N 0 N 0
5 1 2 rusgrnumwwlklem P V N 0 P L N = w N WWalksN G | w 0 = P
6 5 eqeq1d P V N 0 P L N = K N w N WWalksN G | w 0 = P = K N
7 3 4 6 syl2anc G RegUSGraph K V Fin P V N 0 P L N = K N w N WWalksN G | w 0 = P = K N
8 eqid Edg G = Edg G
9 8 wwlksnredwwlkn0 N 0 w N + 1 WWalksN G w 0 = P y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
10 9 ex N 0 w N + 1 WWalksN G w 0 = P y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
11 10 3ad2ant3 V Fin P V N 0 w N + 1 WWalksN G w 0 = P y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
12 11 adantl G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G w 0 = P y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
13 12 imp G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G w 0 = P y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
14 13 rabbidva G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G | w 0 = P = w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
15 14 adantr G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | w 0 = P = w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
16 15 fveq2d G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | w 0 = P = w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
17 simp2 w prefix N + 1 = y y 0 = P lastS y lastS w Edg G y 0 = P
18 17 pm4.71ri w prefix N + 1 = y y 0 = P lastS y lastS w Edg G y 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
19 18 a1i G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G y 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
20 19 rexbidva G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G y N WWalksN G y 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
21 fveq1 x = y x 0 = y 0
22 21 eqeq1d x = y x 0 = P y 0 = P
23 22 rexrab y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G y N WWalksN G y 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
24 20 23 bitr4di G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
25 24 rabbidva G RegUSGraph K V Fin P V N 0 w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = w N + 1 WWalksN G | y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
26 25 adantr G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = w N + 1 WWalksN G | y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
27 26 fveq2d G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = w N + 1 WWalksN G | y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
28 simplr1 G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N V Fin
29 1 eleq1i V Fin Vtx G Fin
30 29 biimpi V Fin Vtx G Fin
31 eqid N + 1 WWalksN G = N + 1 WWalksN G
32 eqid x N WWalksN G | x 0 = P = x N WWalksN G | x 0 = P
33 31 8 32 hashwwlksnext Vtx G Fin w N + 1 WWalksN G | y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = y x N WWalksN G | x 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
34 28 30 33 3syl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | y x N WWalksN G | x 0 = P w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = y x N WWalksN G | x 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
35 fveq1 x = w x 0 = w 0
36 35 eqeq1d x = w x 0 = P w 0 = P
37 36 cbvrabv x N WWalksN G | x 0 = P = w N WWalksN G | w 0 = P
38 37 sumeq1i y x N WWalksN G | x 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
39 38 a1i G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y x N WWalksN G | x 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
40 27 34 39 3eqtrd G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | y N WWalksN G w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
41 rusgrnumwwlkslem y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y lastS y lastS w Edg G = w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G
42 41 eqcomd y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = w N + 1 WWalksN G | w prefix N + 1 = y lastS y lastS w Edg G
43 42 fveq2d y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = w N + 1 WWalksN G | w prefix N + 1 = y lastS y lastS w Edg G
44 43 adantl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = w N + 1 WWalksN G | w prefix N + 1 = y lastS y lastS w Edg G
45 elrabi y w N WWalksN G | w 0 = P y N WWalksN G
46 45 adantl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P y N WWalksN G
47 1 8 wwlksnexthasheq y N WWalksN G w N + 1 WWalksN G | w prefix N + 1 = y lastS y lastS w Edg G = n V | lastS y n Edg G
48 46 47 syl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y lastS y lastS w Edg G = n V | lastS y n Edg G
49 1 rusgrpropadjvtx G RegUSGraph K G USGraph K 0 * p V n V | p n Edg G = K
50 fveq1 w = y w 0 = y 0
51 50 eqeq1d w = y w 0 = P y 0 = P
52 51 elrab y w N WWalksN G | w 0 = P y N WWalksN G y 0 = P
53 1 8 wwlknp y N WWalksN G y Word V y = N + 1 i 0 ..^ N y i y i + 1 Edg G
54 53 adantr y N WWalksN G y 0 = P y Word V y = N + 1 i 0 ..^ N y i y i + 1 Edg G
55 simpll y Word V y = N + 1 V Fin P V N 0 y Word V
56 nn0p1gt0 N 0 0 < N + 1
57 56 3ad2ant3 V Fin P V N 0 0 < N + 1
58 57 adantl y Word V y = N + 1 V Fin P V N 0 0 < N + 1
59 breq2 y = N + 1 0 < y 0 < N + 1
60 59 ad2antlr y Word V y = N + 1 V Fin P V N 0 0 < y 0 < N + 1
61 58 60 mpbird y Word V y = N + 1 V Fin P V N 0 0 < y
62 hashle00 y Word V y 0 y =
63 lencl y Word V y 0
64 63 nn0red y Word V y
65 0re 0
66 lenlt y 0 y 0 ¬ 0 < y
67 66 bicomd y 0 ¬ 0 < y y 0
68 64 65 67 sylancl y Word V ¬ 0 < y y 0
69 nne ¬ y y =
70 69 a1i y Word V ¬ y y =
71 62 68 70 3bitr4rd y Word V ¬ y ¬ 0 < y
72 71 ad2antrr y Word V y = N + 1 V Fin P V N 0 ¬ y ¬ 0 < y
73 72 con4bid y Word V y = N + 1 V Fin P V N 0 y 0 < y
74 61 73 mpbird y Word V y = N + 1 V Fin P V N 0 y
75 55 74 jca y Word V y = N + 1 V Fin P V N 0 y Word V y
76 75 ex y Word V y = N + 1 V Fin P V N 0 y Word V y
77 76 3adant3 y Word V y = N + 1 i 0 ..^ N y i y i + 1 Edg G V Fin P V N 0 y Word V y
78 54 77 syl y N WWalksN G y 0 = P V Fin P V N 0 y Word V y
79 52 78 sylbi y w N WWalksN G | w 0 = P V Fin P V N 0 y Word V y
80 79 imp y w N WWalksN G | w 0 = P V Fin P V N 0 y Word V y
81 lswcl y Word V y lastS y V
82 80 81 syl y w N WWalksN G | w 0 = P V Fin P V N 0 lastS y V
83 82 ad2antrr y w N WWalksN G | w 0 = P V Fin P V N 0 w N WWalksN G | w 0 = P = K N p V n V | p n Edg G = K lastS y V
84 preq1 p = lastS y p n = lastS y n
85 84 eleq1d p = lastS y p n Edg G lastS y n Edg G
86 85 rabbidv p = lastS y n V | p n Edg G = n V | lastS y n Edg G
87 86 fveqeq2d p = lastS y n V | p n Edg G = K n V | lastS y n Edg G = K
88 87 rspcva lastS y V p V n V | p n Edg G = K n V | lastS y n Edg G = K
89 83 88 sylancom y w N WWalksN G | w 0 = P V Fin P V N 0 w N WWalksN G | w 0 = P = K N p V n V | p n Edg G = K n V | lastS y n Edg G = K
90 89 exp41 y w N WWalksN G | w 0 = P V Fin P V N 0 w N WWalksN G | w 0 = P = K N p V n V | p n Edg G = K n V | lastS y n Edg G = K
91 90 com14 p V n V | p n Edg G = K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P n V | lastS y n Edg G = K
92 91 3ad2ant3 G USGraph K 0 * p V n V | p n Edg G = K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P n V | lastS y n Edg G = K
93 49 92 syl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P n V | lastS y n Edg G = K
94 93 imp41 G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P n V | lastS y n Edg G = K
95 44 48 94 3eqtrd G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = K
96 95 sumeq2dv G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = y w N WWalksN G | w 0 = P K
97 oveq1 w N WWalksN G | w 0 = P = K N w N WWalksN G | w 0 = P K = K N K
98 97 adantl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N WWalksN G | w 0 = P K = K N K
99 wwlksnfi Vtx G Fin N WWalksN G Fin
100 29 99 sylbi V Fin N WWalksN G Fin
101 100 3ad2ant1 V Fin P V N 0 N WWalksN G Fin
102 101 ad2antlr G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N N WWalksN G Fin
103 rabfi N WWalksN G Fin w N WWalksN G | w 0 = P Fin
104 102 103 syl G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N WWalksN G | w 0 = P Fin
105 rusgrusgr G RegUSGraph K G USGraph
106 simp1 V Fin P V N 0 V Fin
107 105 106 anim12i G RegUSGraph K V Fin P V N 0 G USGraph V Fin
108 1 isfusgr G FinUSGraph G USGraph V Fin
109 107 108 sylibr G RegUSGraph K V Fin P V N 0 G FinUSGraph
110 simpl G RegUSGraph K V Fin P V N 0 G RegUSGraph K
111 ne0i P V V
112 111 3ad2ant2 V Fin P V N 0 V
113 112 adantl G RegUSGraph K V Fin P V N 0 V
114 1 frusgrnn0 G FinUSGraph G RegUSGraph K V K 0
115 109 110 113 114 syl3anc G RegUSGraph K V Fin P V N 0 K 0
116 115 nn0cnd G RegUSGraph K V Fin P V N 0 K
117 116 adantr G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N K
118 fsumconst w N WWalksN G | w 0 = P Fin K y w N WWalksN G | w 0 = P K = w N WWalksN G | w 0 = P K
119 104 117 118 syl2anc G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P K = w N WWalksN G | w 0 = P K
120 116 4 expp1d G RegUSGraph K V Fin P V N 0 K N + 1 = K N K
121 120 adantr G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N K N + 1 = K N K
122 98 119 121 3eqtr4d G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P K = K N + 1
123 96 122 eqtrd G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N y w N WWalksN G | w 0 = P w N + 1 WWalksN G | w prefix N + 1 = y y 0 = P lastS y lastS w Edg G = K N + 1
124 16 40 123 3eqtrd G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N w N + 1 WWalksN G | w 0 = P = K N + 1
125 peano2nn0 N 0 N + 1 0
126 125 3ad2ant3 V Fin P V N 0 N + 1 0
127 126 adantl G RegUSGraph K V Fin P V N 0 N + 1 0
128 1 2 rusgrnumwwlklem P V N + 1 0 P L N + 1 = w N + 1 WWalksN G | w 0 = P
129 128 eqeq1d P V N + 1 0 P L N + 1 = K N + 1 w N + 1 WWalksN G | w 0 = P = K N + 1
130 3 127 129 syl2anc G RegUSGraph K V Fin P V N 0 P L N + 1 = K N + 1 w N + 1 WWalksN G | w 0 = P = K N + 1
131 130 adantr G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N P L N + 1 = K N + 1 w N + 1 WWalksN G | w 0 = P = K N + 1
132 124 131 mpbird G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N P L N + 1 = K N + 1
133 132 ex G RegUSGraph K V Fin P V N 0 w N WWalksN G | w 0 = P = K N P L N + 1 = K N + 1
134 7 133 sylbid G RegUSGraph K V Fin P V N 0 P L N = K N P L N + 1 = K N + 1