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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	clwwlknonex2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	clwwlknonex2e	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		clwwlknonex2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clwwlknonex2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	clwwlknonex2	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) )
4		isclwwlknon	⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )
5		isclwwlkn	⊢ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) )
6	1	clwwlkbp	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
7	6	simp2d	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 )
8		clwwlkgt0	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 0 < ( ♯ ‘ 𝑊 ) )
9	7 8	jca	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
10	9	adantr	⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
11	5 10	sylbi	⊢ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
12	11	ad2antrl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) )
13		ccat2s1fst	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 0 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
14	12 13	syl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
15		simprr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( 𝑊 ‘ 0 ) = 𝑋 )
16	14 15	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 )
17	16	ex	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 ) )
18	4 17	syl5bi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 ) )
19	18	a1d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 → ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 ) ) )
20	19	3imp	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 )
21		isclwwlknon	⊢ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ‘ 0 ) = 𝑋 ) )
22	3 20 21	sylanbrc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ { 𝑋 , 𝑌 } ∈ 𝐸 ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ) → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ++ ⟨“ 𝑌 ”⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )