Metamath Proof Explorer


Theorem clwwlknonwwlknonb

Description: A word over vertices represents a closed walk of a fixed length N on vertex X iff the word concatenated with X represents a walk of length N on X and X . This theorem would not hold for N = 0 and W = (/) , see clwwlknwwlksnb . (Contributed by AV, 4-Mar-2022) (Revised by AV, 27-Mar-2022)

Ref Expression
Hypothesis clwwlknonwwlknonb.v V = Vtx G
Assertion clwwlknonwwlknonb W Word V N W X ClWWalksNOn G N W ++ ⟨“ X ”⟩ X N WWalksNOn G X

Proof

Step Hyp Ref Expression
1 clwwlknonwwlknonb.v V = Vtx G
2 isclwwlknon W X ClWWalksNOn G N W N ClWWalksN G W 0 = X
3 3anan32 W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X
4 s1eq W 0 = X ⟨“ W 0 ”⟩ = ⟨“ X ”⟩
5 4 oveq2d W 0 = X W ++ ⟨“ W 0 ”⟩ = W ++ ⟨“ X ”⟩
6 5 eleq1d W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N WWalksN G
7 6 biimpac W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ N WWalksN G
8 7 adantl W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ N WWalksN G
9 fvex W 0 V
10 eleq1 W 0 = X W 0 V X V
11 9 10 mpbii W 0 = X X V
12 eqid Edg G = Edg G
13 1 12 wwlknp W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 i 0 ..^ N W ++ ⟨“ X ”⟩ i W ++ ⟨“ X ”⟩ i + 1 Edg G
14 simprrl W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N W Word V
15 simpl W Word V N W Word V
16 15 anim2i X V W Word V N X V W Word V
17 16 ancomd X V W Word V N W Word V X V
18 ccats1alpha W Word V X V W ++ ⟨“ X ”⟩ Word V W Word V X V
19 17 18 syl X V W Word V N W ++ ⟨“ X ”⟩ Word V W Word V X V
20 simpr W Word V X V X V
21 19 20 syl6bi X V W Word V N W ++ ⟨“ X ”⟩ Word V X V
22 21 com12 W ++ ⟨“ X ”⟩ Word V X V W Word V N X V
23 22 adantr W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N X V
24 23 imp W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N X V
25 nnnn0 N N 0
26 ccatws1lenp1b W Word V N 0 W ++ ⟨“ X ”⟩ = N + 1 W = N
27 25 26 sylan2 W Word V N W ++ ⟨“ X ”⟩ = N + 1 W = N
28 27 biimpd W Word V N W ++ ⟨“ X ”⟩ = N + 1 W = N
29 28 adantl X V W Word V N W ++ ⟨“ X ”⟩ = N + 1 W = N
30 29 com12 W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N W = N
31 30 adantl W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N W = N
32 31 imp W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N W = N
33 32 eqcomd W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N N = W
34 14 24 33 3jca W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N W Word V X V N = W
35 34 ex W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 X V W Word V N W Word V X V N = W
36 35 3adant3 W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 i 0 ..^ N W ++ ⟨“ X ”⟩ i W ++ ⟨“ X ”⟩ i + 1 Edg G X V W Word V N W Word V X V N = W
37 13 36 syl W ++ ⟨“ X ”⟩ N WWalksN G X V W Word V N W Word V X V N = W
38 37 expd W ++ ⟨“ X ”⟩ N WWalksN G X V W Word V N W Word V X V N = W
39 11 38 syl5com W 0 = X W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W Word V X V N = W
40 6 39 sylbid W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W Word V N W Word V X V N = W
41 40 com13 W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W Word V X V N = W
42 41 imp32 W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W Word V X V N = W
43 ccats1val2 W Word V X V N = W W ++ ⟨“ X ”⟩ N = X
44 42 43 syl W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ N = X
45 ccat1st1st W Word V W ++ ⟨“ W 0 ”⟩ 0 = W 0
46 45 adantr W Word V N W ++ ⟨“ W 0 ”⟩ 0 = W 0
47 5 fveq1d W 0 = X W ++ ⟨“ W 0 ”⟩ 0 = W ++ ⟨“ X ”⟩ 0
48 47 eqeq1d W 0 = X W ++ ⟨“ W 0 ”⟩ 0 = W 0 W ++ ⟨“ X ”⟩ 0 = W 0
49 48 adantl W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ W 0 ”⟩ 0 = W 0 W ++ ⟨“ X ”⟩ 0 = W 0
50 46 49 syl5ibcom W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ 0 = W 0
51 50 imp W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ 0 = W 0
52 simprr W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W 0 = X
53 51 52 eqtrd W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ 0 = X
54 8 44 53 jca31 W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X
55 54 ex W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X
56 simprl W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 W Word V N W Word V
57 27 biimpcd W ++ ⟨“ X ”⟩ = N + 1 W Word V N W = N
58 57 adantl W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 W Word V N W = N
59 58 imp W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 W Word V N W = N
60 59 eqcomd W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 W Word V N N = W
61 56 60 jca W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 W Word V N W Word V N = W
62 61 ex W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 W Word V N W Word V N = W
63 62 3adant3 W ++ ⟨“ X ”⟩ Word V W ++ ⟨“ X ”⟩ = N + 1 i 0 ..^ N W ++ ⟨“ X ”⟩ i W ++ ⟨“ X ”⟩ i + 1 Edg G W Word V N W Word V N = W
64 13 63 syl W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W Word V N = W
65 64 imp W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W Word V N = W
66 eleq1 N = W N W
67 lbfzo0 0 0 ..^ W W
68 67 biimpri W 0 0 ..^ W
69 66 68 syl6bi N = W N 0 0 ..^ W
70 69 com12 N N = W 0 0 ..^ W
71 70 ad2antll W ++ ⟨“ X ”⟩ N WWalksN G W Word V N N = W 0 0 ..^ W
72 71 anim2d W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W Word V N = W W Word V 0 0 ..^ W
73 65 72 mpd W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W Word V 0 0 ..^ W
74 ccats1val1 W Word V 0 0 ..^ W W ++ ⟨“ X ”⟩ 0 = W 0
75 73 74 syl W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W ++ ⟨“ X ”⟩ 0 = W 0
76 75 eqeq1d W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W ++ ⟨“ X ”⟩ 0 = X W 0 = X
77 76 biimpd W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W ++ ⟨“ X ”⟩ 0 = X W 0 = X
78 77 ex W ++ ⟨“ X ”⟩ N WWalksN G W Word V N W ++ ⟨“ X ”⟩ 0 = X W 0 = X
79 78 adantr W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W Word V N W ++ ⟨“ X ”⟩ 0 = X W 0 = X
80 79 com3r W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W Word V N W 0 = X
81 80 impcom W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X W Word V N W 0 = X
82 6 biimparc W ++ ⟨“ X ”⟩ N WWalksN G W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G
83 simpr W ++ ⟨“ X ”⟩ N WWalksN G W 0 = X W 0 = X
84 82 83 jca W ++ ⟨“ X ”⟩ N WWalksN G W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X
85 84 ex W ++ ⟨“ X ”⟩ N WWalksN G W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X
86 85 ad2antrr W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X
87 81 86 syldc W Word V N W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X
88 55 87 impbid W Word V N W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ X ”⟩ 0 = X
89 3 88 bitr4id W Word V N W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ X ”⟩ N = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X
90 1 clwwlknwwlksnb W Word V N W N ClWWalksN G W ++ ⟨“ W 0 ”⟩ N WWalksN G
91 90 anbi1d W Word V N W N ClWWalksN G W 0 = X W ++ ⟨“ W 0 ”⟩ N WWalksN G W 0 = X
92 89 91 bitr4d W Word V N W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ X ”⟩ N = X W N ClWWalksN G W 0 = X
93 2 92 bitr4id W Word V N W X ClWWalksNOn G N W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ X ”⟩ N = X
94 wwlknon W ++ ⟨“ X ”⟩ X N WWalksNOn G X W ++ ⟨“ X ”⟩ N WWalksN G W ++ ⟨“ X ”⟩ 0 = X W ++ ⟨“ X ”⟩ N = X
95 93 94 bitr4di W Word V N W X ClWWalksNOn G N W ++ ⟨“ X ”⟩ X N WWalksNOn G X