Metamath Proof Explorer


Theorem clwwlknonex2

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Hypotheses clwwlknonex2.v V = Vtx G
clwwlknonex2.e E = Edg G
Assertion clwwlknonex2 X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v V = Vtx G
2 clwwlknonex2.e E = Edg G
3 uz3m2nn N 3 N 2
4 3 nnne0d N 3 N 2 0
5 4 3ad2ant3 X V Y V N 3 N 2 0
6 1 2 clwwlknonel N 2 0 W X ClWWalksNOn G N 2 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X
7 5 6 syl X V Y V N 3 W X ClWWalksNOn G N 2 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X
8 simpr11 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W Word V
9 8 adantr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W Word V
10 simpll1 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E X V
11 simpll2 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E Y V
12 ccatw2s1cl W Word V X V Y V W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V
13 9 10 11 12 syl3anc X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V
14 1 2 clwwlknonex2lem2 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E i 0 ..^ W 1 W 1 W W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E
15 simp11 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W Word V
16 15 ad2antlr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W Word V
17 ccatw2s1len W Word V W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
18 16 17 syl X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
19 18 oveq1d X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 = W + 2 - 1
20 19 oveq2d X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 = 0 ..^ W + 2 - 1
21 simp3 X V Y V N 3 N 3
22 simp2 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W = N 2
23 21 22 anim12i X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X N 3 W = N 2
24 23 adantr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E N 3 W = N 2
25 clwwlknonex2lem1 N 3 W = N 2 0 ..^ W + 2 - 1 = 0 ..^ W 1 W 1 W
26 24 25 syl X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E 0 ..^ W + 2 - 1 = 0 ..^ W 1 W 1 W
27 20 26 eqtrd X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 = 0 ..^ W 1 W 1 W
28 14 27 raleqtrrdv X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E
29 ccatws1cl W Word V X V W ++ ⟨“ X ”⟩ Word V
30 lswccats1 W ++ ⟨“ X ”⟩ Word V Y V lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
31 29 30 stoic3 W Word V X V Y V lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
32 16 10 11 31 syl3anc X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = Y
33 3 nngt0d N 3 0 < N 2
34 breq2 W = N 2 0 < W 0 < N 2
35 33 34 imbitrrid W = N 2 N 3 0 < W
36 35 3ad2ant2 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X N 3 0 < W
37 36 com12 N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X 0 < W
38 37 3ad2ant3 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X 0 < W
39 38 imp X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X 0 < W
40 39 adantr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E 0 < W
41 ccat2s1fst W Word V 0 < W W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = W 0
42 16 40 41 syl2anc X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = W 0
43 32 42 preq12d X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = Y W 0
44 prcom X Y = Y X
45 44 eleq1i X Y E Y X E
46 45 biimpi X Y E Y X E
47 46 adantl X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E Y X E
48 preq2 W 0 = X Y W 0 = Y X
49 48 eleq1d W 0 = X Y W 0 E Y X E
50 49 3ad2ant3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X Y W 0 E Y X E
51 50 ad2antlr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E Y W 0 E Y X E
52 47 51 mpbird X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E Y W 0 E
53 43 52 eqeltrd X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E
54 13 28 53 3jca X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E
55 17 3ad2ant1 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
56 55 3ad2ant1 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
57 56 ad2antlr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = W + 2
58 oveq1 W = N 2 W + 2 = N - 2 + 2
59 eluzelcn N 3 N
60 2cn 2
61 npcan N 2 N - 2 + 2 = N
62 59 60 61 sylancl N 3 N - 2 + 2 = N
63 58 62 sylan9eq W = N 2 N 3 W + 2 = N
64 63 ex W = N 2 N 3 W + 2 = N
65 64 3ad2ant2 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X N 3 W + 2 = N
66 65 com12 N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W + 2 = N
67 66 3ad2ant3 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W + 2 = N
68 67 imp X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X W + 2 = N
69 68 adantr X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W + 2 = N
70 57 69 eqtrd X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
71 54 70 jca X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
72 71 exp31 X V Y V N 3 W Word V i 0 ..^ W 1 W i W i + 1 E lastS W W 0 E W = N 2 W 0 = X X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
73 7 72 sylbid X V Y V N 3 W X ClWWalksNOn G N 2 X Y E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
74 73 com23 X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
75 74 3imp X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
76 eluzge3nn N 3 N
77 1 2 isclwwlknx N W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
78 76 77 syl N 3 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
79 78 3ad2ant3 X V Y V N 3 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
80 79 3ad2ant1 X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ Word V i 0 ..^ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 1 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ i + 1 E lastS W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 E W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = N
81 75 80 mpbird X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G