Metamath Proof Explorer


Theorem clwwlknonex2e

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk on vertex X . (Contributed by AV, 17-Apr-2022)

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

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v V = Vtx G
2 clwwlknonex2.e E = Edg G
3 1 2 clwwlknonex2 X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G
4 isclwwlknon W X ClWWalksNOn G N 2 W N 2 ClWWalksN G W 0 = X
5 isclwwlkn W N 2 ClWWalksN G W ClWWalks G W = N 2
6 1 clwwlkbp W ClWWalks G G V W Word V W
7 6 simp2d W ClWWalks G W Word V
8 clwwlkgt0 W ClWWalks G 0 < W
9 7 8 jca W ClWWalks G W Word V 0 < W
10 9 adantr W ClWWalks G W = N 2 W Word V 0 < W
11 5 10 sylbi W N 2 ClWWalksN G W Word V 0 < W
12 11 ad2antrl X V Y V N 3 W N 2 ClWWalksN G W 0 = X W Word V 0 < W
13 ccat2s1fst W Word V 0 < W W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = W 0
14 12 13 syl X V Y V N 3 W N 2 ClWWalksN G W 0 = X W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = W 0
15 simprr X V Y V N 3 W N 2 ClWWalksN G W 0 = X W 0 = X
16 14 15 eqtrd X V Y V N 3 W N 2 ClWWalksN G W 0 = X W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X
17 16 ex X V Y V N 3 W N 2 ClWWalksN G W 0 = X W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X
18 4 17 syl5bi X V Y V N 3 W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X
19 18 a1d X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X
20 19 3imp X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X
21 isclwwlknon W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ X ClWWalksNOn G N W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ N ClWWalksN G W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ 0 = X
22 3 20 21 sylanbrc X V Y V N 3 X Y E W X ClWWalksNOn G N 2 W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ X ClWWalksNOn G N