| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isclwwlknon |
⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ↔ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ) |
| 2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 3 |
2
|
clwwlknbp |
⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) |
| 4 |
|
simpll |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ) |
| 5 |
|
uzuzle23 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) |
| 6 |
|
eluzfz2 |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ( 2 ... 𝑁 ) ) |
| 7 |
5 6
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( 2 ... 𝑁 ) ) |
| 8 |
7
|
adantl |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ∈ ( 2 ... 𝑁 ) ) |
| 9 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 2 ... ( ♯ ‘ 𝑊 ) ) = ( 2 ... 𝑁 ) ) |
| 10 |
9
|
eleq2d |
⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 2 ... 𝑁 ) ) ) |
| 11 |
10
|
ad2antlr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ↔ 𝑁 ∈ ( 2 ... 𝑁 ) ) ) |
| 12 |
8 11
|
mpbird |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) |
| 13 |
4 12
|
jca |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) ) |
| 14 |
13
|
ex |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) ) ) |
| 15 |
3 14
|
syl |
⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) ) ) |
| 16 |
15
|
adantr |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) ) ) |
| 17 |
1 16
|
sylbi |
⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) ) ) |
| 18 |
17
|
impcom |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) → ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) ) |
| 19 |
|
swrds2m |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( 2 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) = ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 20 |
18 19
|
syl |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) = ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 21 |
20
|
3adant3 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) = ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 22 |
|
simp3 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) |
| 23 |
|
eqidd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) ) |
| 24 |
22 23
|
s2eqd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 25 |
|
simpr |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ‘ 0 ) = 𝑋 ) |
| 26 |
|
eqidd |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) ) |
| 27 |
25 26
|
s2eqd |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ = ⟨“ 𝑋 ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 28 |
1 27
|
sylbi |
⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ = ⟨“ 𝑋 ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 29 |
28
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ = ⟨“ 𝑋 ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 30 |
21 24 29
|
3eqtrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) = ⟨“ 𝑋 ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) |
| 31 |
|
clwwlknonmpo |
⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) , 𝑛 ∈ ℕ0 ↦ { 𝑤 ∈ ( 𝑛 ClWWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) |
| 32 |
31
|
elmpocl1 |
⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) |
| 33 |
32
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → 𝑋 ∈ ( Vtx ‘ 𝐺 ) ) |
| 34 |
|
eluzge3nn |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ ) |
| 35 |
|
fzo0end |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 36 |
34 35
|
syl |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 37 |
36
|
adantl |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) |
| 38 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝑁 ) ) |
| 39 |
38
|
ad2antlr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝑁 ) ) |
| 40 |
39
|
eleq2d |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 − 1 ) ∈ ( 0 ..^ 𝑁 ) ) ) |
| 41 |
37 40
|
mpbird |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
| 42 |
|
wrdsymbcl |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) |
| 43 |
4 41 42
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) |
| 44 |
43
|
ex |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 45 |
3 44
|
syl |
⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 46 |
45
|
adantr |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 47 |
1 46
|
sylbi |
⊢ ( 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ) |
| 48 |
47
|
impcom |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) |
| 49 |
48
|
3adant3 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ) |
| 50 |
|
preq1 |
⊢ ( ( 𝑊 ‘ 0 ) = 𝑋 → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } = { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ) |
| 51 |
50
|
adantl |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } = { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ) |
| 52 |
51
|
eqcomd |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ) |
| 53 |
52
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } = { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ) |
| 54 |
|
prcom |
⊢ { ( 𝑊 ‘ 0 ) , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } |
| 55 |
53 54
|
eqtrdi |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ) |
| 56 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
| 57 |
2 56
|
clwwlknp |
⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 58 |
57
|
adantr |
⊢ ( ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 59 |
58
|
3ad2ant2 |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 60 |
|
lsw |
⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
| 61 |
|
fvoveq1 |
⊢ ( ( ♯ ‘ 𝑊 ) = 𝑁 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) ) |
| 62 |
60 61
|
sylan9eq |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) ) |
| 63 |
62
|
adantr |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( 𝑁 − 1 ) ) ) |
| 64 |
63
|
preq1d |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) ) → { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ) |
| 65 |
64
|
eleq1d |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 66 |
65
|
biimpd |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 67 |
66
|
ex |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
| 68 |
67
|
com23 |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
| 69 |
68
|
a1d |
⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) → ( { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) ) |
| 70 |
69
|
3imp |
⊢ ( ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ∧ { ( lastS ‘ 𝑊 ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 71 |
59 70
|
mpcom |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { ( 𝑊 ‘ ( 𝑁 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 72 |
55 71
|
eqeltrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ 0 ) = 𝑋 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 73 |
1 72
|
syl3an2b |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
| 74 |
|
eqid |
⊢ ( ClWWalksNOn ‘ 𝐺 ) = ( ClWWalksNOn ‘ 𝐺 ) |
| 75 |
74 2 56
|
s2elclwwlknon2 |
⊢ ( ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 1 ) ) ∈ ( Vtx ‘ 𝐺 ) ∧ { 𝑋 , ( 𝑊 ‘ ( 𝑁 − 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) → ⟨“ 𝑋 ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) |
| 76 |
33 49 73 75
|
syl3anc |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ⟨“ 𝑋 ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) |
| 77 |
30 76
|
eqeltrd |
⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 𝑁 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 substr ⟨ ( 𝑁 − 2 ) , 𝑁 ⟩ ) ∈ ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) 2 ) ) |