Metamath Proof Explorer

Theorem 2clwwlk2clwwlk

Description: An element of the value of operation C , i.e., a word being a double loop of length N on vertex X , is composed of two closed walks. (Contributed by AV, 28-Apr-2022) (Proof shortened by AV, 3-Nov-2022)

Ref Expression
Hypothesis 2clwwlk.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
Assertion 2clwwlk2clwwlk ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ∃ 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∃ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) 𝑊 = ( 𝑎 ++ 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 2clwwlk.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
2 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
3 1 2clwwlkel ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
4 2 3 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
5 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
6 5 anim1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
7 3anass ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
8 6 7 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
9 clwwnonrepclwwnon ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
10 8 9 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) )
11 5 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
12 simprl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
13 simprr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 )
14 isclwwlknon ⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) )
15 simpr ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ‘ 0 ) = 𝑋 )
16 15 eqcomd ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → 𝑋 = ( 𝑊 ‘ 0 ) )
17 14 16 sylbi ⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → 𝑋 = ( 𝑊 ‘ 0 ) )
18 17 ad2antrl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑋 = ( 𝑊 ‘ 0 ) )
19 13 18 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) )
20 2clwwlk2clwwlklem ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) )
21 11 12 19 20 syl3anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) )
22 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
23 22 clwwlknbp ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
24 opeq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ = ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ )
25 24 oveq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) = ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) )
26 25 oveq2d ⊢ ( 𝑁 = ( ♯ ‘ 𝑊 ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
27 26 eqcoms ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
28 27 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
29 simpl ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) )
30 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
31 ige3m2fz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) )
32 30 31 sseldi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 0 ... 𝑁 ) )
33 32 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 2 ) ∈ ( 0 ... 𝑁 ) )
34 33 adantl ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑁 − 2 ) ∈ ( 0 ... 𝑁 ) )
35 oveq2 ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 0 ... ( ♯ ‘ 𝑊 ) ) = ( 0 ... 𝑁 ) )
36 35 eleq2d ⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( ( 𝑁 − 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ... 𝑁 ) ) )
37 36 ad2antlr ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑁 − 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ... 𝑁 ) ) )
38 34 37 mpbird ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑁 − 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
39 pfxcctswrd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 − 2 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = 𝑊 )
40 29 38 39 syl2an2r ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = 𝑊 )
41 28 40 eqtrd ⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 )
42 23 41 sylan ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 )
43 42 ex ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 ) )
44 43 adantr ⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 ) )
45 14 44 sylbi ⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 ) )
46 45 adantr ⊢ ( ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 ) )
47 46 impcom ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) = 𝑊 )
48 47 eqcomd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) )
49 10 21 48 3jca ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∧ 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) ) )
50 49 ex ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∧ 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) ) ) )
51 4 50 sylbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) → ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∧ 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) ) ) )
52 rspceov ⊢ ( ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ∧ 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ) ) → ∃ 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∃ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) 𝑊 = ( 𝑎 ++ 𝑏 ) )
53 51 52 syl6 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) → ∃ 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∃ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) 𝑊 = ( 𝑎 ++ 𝑏 ) ) )
54 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
55 2cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℂ )
56 54 55 npcand ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
57 56 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
58 57 oveq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( ( 𝑁 − 2 ) + 2 ) ) = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
59 58 eleq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( ( 𝑁 − 2 ) + 2 ) ) ↔ ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
60 59 biimpd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( ( 𝑁 − 2 ) + 2 ) ) → ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) )
61 clwwlknonccat ⊢ ( ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) → ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( ( 𝑁 − 2 ) + 2 ) ) )
62 60 61 impel ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ) → ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) )
63 isclwwlknon ⊢ ( 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ↔ ( 𝑏 ∈ ( 2 ClWWalksN 𝐺 ) ∧ ( 𝑏 ‘ 0 ) = 𝑋 ) )
64 clwwlkn2 ⊢ ( 𝑏 ∈ ( 2 ClWWalksN 𝐺 ) ↔ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑏 ‘ 0 ) , ( 𝑏 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
65 isclwwlknon ⊢ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ↔ ( 𝑎 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) )
66 22 clwwlknbp ⊢ ( 𝑎 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) → ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) )
67 simpl ⊢ ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) → 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) )
68 simprr ⊢ ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) → 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) )
69 2nn ⊢ 2 ∈ ℕ
70 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ )
71 69 70 mpbir ⊢ 0 ∈ ( 0 ..^ 2 )
72 oveq2 ⊢ ( ( ♯ ‘ 𝑏 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝑏 ) ) = ( 0 ..^ 2 ) )
73 71 72 eleqtrrid ⊢ ( ( ♯ ‘ 𝑏 ) = 2 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑏 ) ) )
74 73 ad2antrl ⊢ ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑏 ) ) )
75 67 68 74 3jca ⊢ ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) → ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑏 ) ) ) )
76 75 adantr ⊢ ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) → ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑏 ) ) ) )
77 76 adantr ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑏 ) ) ) )
78 ccatval3 ⊢ ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑏 ) ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 0 + ( ♯ ‘ 𝑎 ) ) ) = ( 𝑏 ‘ 0 ) )
79 77 78 syl ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 0 + ( ♯ ‘ 𝑎 ) ) ) = ( 𝑏 ‘ 0 ) )
80 simpr ⊢ ( ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) )
81 80 oveq2d ⊢ ( ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( 0 + ( ♯ ‘ 𝑎 ) ) = ( 0 + ( 𝑁 − 2 ) ) )
82 81 adantl ⊢ ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) → ( 0 + ( ♯ ‘ 𝑎 ) ) = ( 0 + ( 𝑁 − 2 ) ) )
83 54 55 subcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℂ )
84 83 addid2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 0 + ( 𝑁 − 2 ) ) = ( 𝑁 − 2 ) )
85 84 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 0 + ( 𝑁 − 2 ) ) = ( 𝑁 − 2 ) )
86 82 85 sylan9eq ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 0 + ( ♯ ‘ 𝑎 ) ) = ( 𝑁 − 2 ) )
87 86 eqcomd ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( 𝑁 − 2 ) = ( 0 + ( ♯ ‘ 𝑎 ) ) )
88 87 fveq2d ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = ( ( 𝑎 ++ 𝑏 ) ‘ ( 0 + ( ♯ ‘ 𝑎 ) ) ) )
89 simpl ⊢ ( ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( 𝑏 ‘ 0 ) = 𝑋 )
90 89 eqcomd ⊢ ( ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → 𝑋 = ( 𝑏 ‘ 0 ) )
91 90 ad2antlr ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → 𝑋 = ( 𝑏 ‘ 0 ) )
92 79 88 91 3eqtr4d ⊢ ( ( ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( 𝑏 ‘ 0 ) = 𝑋 ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 )
93 92 exp53 ⊢ ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) ) )
94 93 com24 ⊢ ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) ) )
95 94 imp ⊢ ( ( 𝑎 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑎 ) = ( 𝑁 − 2 ) ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
96 66 95 syl ⊢ ( 𝑎 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
97 96 adantr ⊢ ( ( 𝑎 ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) ∧ ( 𝑎 ‘ 0 ) = 𝑋 ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
98 65 97 sylbi ⊢ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
99 98 com13 ⊢ ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
100 99 3adant3 ⊢ ( ( ( ♯ ‘ 𝑏 ) = 2 ∧ 𝑏 ∈ Word ( Vtx ‘ 𝐺 ) ∧ { ( 𝑏 ‘ 0 ) , ( 𝑏 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
101 64 100 sylbi ⊢ ( 𝑏 ∈ ( 2 ClWWalksN 𝐺 ) → ( ( 𝑏 ‘ 0 ) = 𝑋 → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
102 101 imp ⊢ ( ( 𝑏 ∈ ( 2 ClWWalksN 𝐺 ) ∧ ( 𝑏 ‘ 0 ) = 𝑋 ) → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
103 63 102 sylbi ⊢ ( 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) → ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
104 103 impcom ⊢ ( ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) )
105 104 impcom ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ) → ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 )
106 1 2clwwlkel ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
107 2 106 sylan2 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
108 107 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ) → ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( ( 𝑎 ++ 𝑏 ) ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) )
109 62 105 108 mpbir2and ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ) → ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 𝐶 𝑁 ) )
110 eleq1 ⊢ ( 𝑊 = ( 𝑎 ++ 𝑏 ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑎 ++ 𝑏 ) ∈ ( 𝑋 𝐶 𝑁 ) ) )
111 109 110 syl5ibrcom ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ ( 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∧ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) ) → ( 𝑊 = ( 𝑎 ++ 𝑏 ) → 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ) )
112 111 rexlimdvva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ∃ 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∃ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) 𝑊 = ( 𝑎 ++ 𝑏 ) → 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ) )
113 53 112 impbid ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ∃ 𝑎 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) ) ∃ 𝑏 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) 𝑊 = ( 𝑎 ++ 𝑏 ) ) )