Metamath Proof Explorer

Theorem 2clwwlk2clwwlklem

Description: Lemma for 2clwwlk2clwwlk . (Contributed by AV, 27-Apr-2022)

Ref Expression
Assertion 2clwwlk2clwwlklem ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→WsubstrN−2N∈XClWWalksNOn⁡G2

Proof

Step Hyp Ref Expression
1 isclwwlknon ⊢W∈XClWWalksNOn⁡GN↔W∈NClWWalksNG∧W⁡0=X
2 eqid ⊢Vtx⁡G=Vtx⁡G
3 2 clwwlknbp ⊢W∈NClWWalksNG→W∈WordVtx⁡G∧W=N
4 simpll ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→W∈WordVtx⁡G
5 uzuzle23 ⊢N∈ℤ≥3→N∈ℤ≥2
6 eluzfz2 ⊢N∈ℤ≥2→N∈2…N
7 5 6 syl ⊢N∈ℤ≥3→N∈2…N
8 7 adantl ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→N∈2…N
9 oveq2 ⊢W=N→2…W=2…N
10 9 eleq2d ⊢W=N→N∈2…W↔N∈2…N
11 10 ad2antlr ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→N∈2…W↔N∈2…N
12 8 11 mpbird ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→N∈2…W
13 4 12 jca ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→W∈WordVtx⁡G∧N∈2…W
14 13 ex ⊢W∈WordVtx⁡G∧W=N→N∈ℤ≥3→W∈WordVtx⁡G∧N∈2…W
15 3 14 syl ⊢W∈NClWWalksNG→N∈ℤ≥3→W∈WordVtx⁡G∧N∈2…W
16 15 adantr ⊢W∈NClWWalksNG∧W⁡0=X→N∈ℤ≥3→W∈WordVtx⁡G∧N∈2…W
17 1 16 sylbi ⊢W∈XClWWalksNOn⁡GN→N∈ℤ≥3→W∈WordVtx⁡G∧N∈2…W
18 17 impcom ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN→W∈WordVtx⁡G∧N∈2…W
19 swrds2m ⊢W∈WordVtx⁡G∧N∈2…W→WsubstrN−2N=⟨“W⁡N−2W⁡N−1”⟩
20 18 19 syl ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN→WsubstrN−2N=⟨“W⁡N−2W⁡N−1”⟩
21 20 3adant3 ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→WsubstrN−2N=⟨“W⁡N−2W⁡N−1”⟩
22 simp3 ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→W⁡N−2=W⁡0
23 eqidd ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→W⁡N−1=W⁡N−1
24 22 23 s2eqd ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→⟨“W⁡N−2W⁡N−1”⟩=⟨“W⁡0W⁡N−1”⟩
25 simpr ⊢W∈NClWWalksNG∧W⁡0=X→W⁡0=X
26 eqidd ⊢W∈NClWWalksNG∧W⁡0=X→W⁡N−1=W⁡N−1
27 25 26 s2eqd ⊢W∈NClWWalksNG∧W⁡0=X→⟨“W⁡0W⁡N−1”⟩=⟨“XW⁡N−1”⟩
28 1 27 sylbi ⊢W∈XClWWalksNOn⁡GN→⟨“W⁡0W⁡N−1”⟩=⟨“XW⁡N−1”⟩
29 28 3ad2ant2 ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→⟨“W⁡0W⁡N−1”⟩=⟨“XW⁡N−1”⟩
30 21 24 29 3eqtrd ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→WsubstrN−2N=⟨“XW⁡N−1”⟩
31 clwwlknonmpo ⊢ClWWalksNOn⁡G=v∈Vtx⁡G,n∈ℕ0⟼w∈nClWWalksNG|w⁡0=v
32 31 elmpocl1 ⊢W∈XClWWalksNOn⁡GN→X∈Vtx⁡G
33 32 3ad2ant2 ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→X∈Vtx⁡G
34 eluzge3nn ⊢N∈ℤ≥3→N∈ℕ
35 fzo0end ⊢N∈ℕ→N−1∈0..^N
36 34 35 syl ⊢N∈ℤ≥3→N−1∈0..^N
37 36 adantl ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→N−1∈0..^N
38 oveq2 ⊢W=N→0..^W=0..^N
39 38 ad2antlr ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→0..^W=0..^N
40 39 eleq2d ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→N−1∈0..^W↔N−1∈0..^N
41 37 40 mpbird ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→N−1∈0..^W
42 wrdsymbcl ⊢W∈WordVtx⁡G∧N−1∈0..^W→W⁡N−1∈Vtx⁡G
43 4 41 42 syl2anc ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3→W⁡N−1∈Vtx⁡G
44 43 ex ⊢W∈WordVtx⁡G∧W=N→N∈ℤ≥3→W⁡N−1∈Vtx⁡G
45 3 44 syl ⊢W∈NClWWalksNG→N∈ℤ≥3→W⁡N−1∈Vtx⁡G
46 45 adantr ⊢W∈NClWWalksNG∧W⁡0=X→N∈ℤ≥3→W⁡N−1∈Vtx⁡G
47 1 46 sylbi ⊢W∈XClWWalksNOn⁡GN→N∈ℤ≥3→W⁡N−1∈Vtx⁡G
48 47 impcom ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN→W⁡N−1∈Vtx⁡G
49 48 3adant3 ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→W⁡N−1∈Vtx⁡G
50 preq1 ⊢W⁡0=X→W⁡0W⁡N−1=XW⁡N−1
51 50 adantl ⊢W∈NClWWalksNG∧W⁡0=X→W⁡0W⁡N−1=XW⁡N−1
52 51 eqcomd ⊢W∈NClWWalksNG∧W⁡0=X→XW⁡N−1=W⁡0W⁡N−1
53 52 3ad2ant2 ⊢N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→XW⁡N−1=W⁡0W⁡N−1
54 prcom ⊢W⁡0W⁡N−1=W⁡N−1W⁡0
55 53 54 eqtrdi ⊢N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→XW⁡N−1=W⁡N−1W⁡0
56 eqid ⊢Edg⁡G=Edg⁡G
57 2 56 clwwlknp ⊢W∈NClWWalksNG→W∈WordVtx⁡G∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
58 57 adantr ⊢W∈NClWWalksNG∧W⁡0=X→W∈WordVtx⁡G∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
59 58 3ad2ant2 ⊢N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→W∈WordVtx⁡G∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
60 lsw ⊢W∈WordVtx⁡G→lastS⁡W=W⁡W−1
61 fvoveq1 ⊢W=N→W⁡W−1=W⁡N−1
62 60 61 sylan9eq ⊢W∈WordVtx⁡G∧W=N→lastS⁡W=W⁡N−1
63 62 adantr ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→lastS⁡W=W⁡N−1
64 63 preq1d ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→lastS⁡WW⁡0=W⁡N−1W⁡0
65 64 eleq1d ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→lastS⁡WW⁡0∈Edg⁡G↔W⁡N−1W⁡0∈Edg⁡G
66 65 biimpd ⊢W∈WordVtx⁡G∧W=N∧N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→lastS⁡WW⁡0∈Edg⁡G→W⁡N−1W⁡0∈Edg⁡G
67 66 ex ⊢W∈WordVtx⁡G∧W=N→N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→lastS⁡WW⁡0∈Edg⁡G→W⁡N−1W⁡0∈Edg⁡G
68 67 com23 ⊢W∈WordVtx⁡G∧W=N→lastS⁡WW⁡0∈Edg⁡G→N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→W⁡N−1W⁡0∈Edg⁡G
69 68 a1d ⊢W∈WordVtx⁡G∧W=N→∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G→lastS⁡WW⁡0∈Edg⁡G→N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→W⁡N−1W⁡0∈Edg⁡G
70 69 3imp ⊢W∈WordVtx⁡G∧W=N∧∀i∈0..^N−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G→N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→W⁡N−1W⁡0∈Edg⁡G
71 59 70 mpcom ⊢N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→W⁡N−1W⁡0∈Edg⁡G
72 55 71 eqeltrd ⊢N∈ℤ≥3∧W∈NClWWalksNG∧W⁡0=X∧W⁡N−2=W⁡0→XW⁡N−1∈Edg⁡G
73 1 72 syl3an2b ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→XW⁡N−1∈Edg⁡G
74 eqid ⊢ClWWalksNOn⁡G=ClWWalksNOn⁡G
75 74 2 56 s2elclwwlknon2 ⊢X∈Vtx⁡G∧W⁡N−1∈Vtx⁡G∧XW⁡N−1∈Edg⁡G→⟨“XW⁡N−1”⟩∈XClWWalksNOn⁡G2
76 33 49 73 75 syl3anc ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→⟨“XW⁡N−1”⟩∈XClWWalksNOn⁡G2
77 30 76 eqeltrd ⊢N∈ℤ≥3∧W∈XClWWalksNOn⁡GN∧W⁡N−2=W⁡0→WsubstrN−2N∈XClWWalksNOn⁡G2