Metamath Proof Explorer


Theorem iswwlksnon

Description: The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis iswwlksnon.v V = Vtx G
Assertion iswwlksnon A N WWalksNOn G B = w N WWalksN G | w 0 = A w N = B

Proof

Step Hyp Ref Expression
1 iswwlksnon.v V = Vtx G
2 0ov A B =
3 df-wwlksnon WWalksNOn = n 0 , g V a Vtx g , b Vtx g w n WWalksN g | w 0 = a w n = b
4 3 mpondm0 ¬ N 0 G V N WWalksNOn G =
5 4 oveqd ¬ N 0 G V A N WWalksNOn G B = A B
6 df-wwlksn WWalksN = n 0 , g V w WWalks g | w = n + 1
7 6 mpondm0 ¬ N 0 G V N WWalksN G =
8 7 rabeqdv ¬ N 0 G V w N WWalksN G | w 0 = A w N = B = w | w 0 = A w N = B
9 rab0 w | w 0 = A w N = B =
10 8 9 eqtrdi ¬ N 0 G V w N WWalksN G | w 0 = A w N = B =
11 2 5 10 3eqtr4a ¬ N 0 G V A N WWalksNOn G B = w N WWalksN G | w 0 = A w N = B
12 1 wwlksnon N 0 G V N WWalksNOn G = a V , b V w N WWalksN G | w 0 = a w N = b
13 12 adantr N 0 G V ¬ A V B V N WWalksNOn G = a V , b V w N WWalksN G | w 0 = a w N = b
14 13 oveqd N 0 G V ¬ A V B V A N WWalksNOn G B = A a V , b V w N WWalksN G | w 0 = a w N = b B
15 eqid a V , b V w N WWalksN G | w 0 = a w N = b = a V , b V w N WWalksN G | w 0 = a w N = b
16 15 mpondm0 ¬ A V B V A a V , b V w N WWalksN G | w 0 = a w N = b B =
17 16 adantl N 0 G V ¬ A V B V A a V , b V w N WWalksN G | w 0 = a w N = b B =
18 14 17 eqtrd N 0 G V ¬ A V B V A N WWalksNOn G B =
19 18 ex N 0 G V ¬ A V B V A N WWalksNOn G B =
20 5 2 eqtrdi ¬ N 0 G V A N WWalksNOn G B =
21 20 a1d ¬ N 0 G V ¬ A V B V A N WWalksNOn G B =
22 19 21 pm2.61i ¬ A V B V A N WWalksNOn G B =
23 1 wwlknllvtx w N WWalksN G w 0 V w N V
24 eleq1 A = w 0 A V w 0 V
25 24 eqcoms w 0 = A A V w 0 V
26 eleq1 B = w N B V w N V
27 26 eqcoms w N = B B V w N V
28 25 27 bi2anan9 w 0 = A w N = B A V B V w 0 V w N V
29 23 28 syl5ibrcom w N WWalksN G w 0 = A w N = B A V B V
30 29 con3rr3 ¬ A V B V w N WWalksN G ¬ w 0 = A w N = B
31 30 ralrimiv ¬ A V B V w N WWalksN G ¬ w 0 = A w N = B
32 rabeq0 w N WWalksN G | w 0 = A w N = B = w N WWalksN G ¬ w 0 = A w N = B
33 31 32 sylibr ¬ A V B V w N WWalksN G | w 0 = A w N = B =
34 22 33 eqtr4d ¬ A V B V A N WWalksNOn G B = w N WWalksN G | w 0 = A w N = B
35 12 adantr N 0 G V A V B V N WWalksNOn G = a V , b V w N WWalksN G | w 0 = a w N = b
36 eqeq2 a = A w 0 = a w 0 = A
37 eqeq2 b = B w N = b w N = B
38 36 37 bi2anan9 a = A b = B w 0 = a w N = b w 0 = A w N = B
39 38 rabbidv a = A b = B w N WWalksN G | w 0 = a w N = b = w N WWalksN G | w 0 = A w N = B
40 39 adantl N 0 G V A V B V a = A b = B w N WWalksN G | w 0 = a w N = b = w N WWalksN G | w 0 = A w N = B
41 simprl N 0 G V A V B V A V
42 simprr N 0 G V A V B V B V
43 ovex N WWalksN G V
44 43 rabex w N WWalksN G | w 0 = A w N = B V
45 44 a1i N 0 G V A V B V w N WWalksN G | w 0 = A w N = B V
46 35 40 41 42 45 ovmpod N 0 G V A V B V A N WWalksNOn G B = w N WWalksN G | w 0 = A w N = B
47 11 34 46 ecase A N WWalksNOn G B = w N WWalksN G | w 0 = A w N = B