Metamath Proof Explorer

Theorem clwwlkn2

Description: A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 25-Apr-2021)

Ref Expression
Assertion clwwlkn2 ⊢ W ∈ 2 ClWWalksN G ↔ W = 2 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 2 3 isclwwlknx ⊢ 2 ∈ ℕ → W ∈ 2 ClWWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = 2
5 1 4 ax-mp ⊢ W ∈ 2 ClWWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = 2
6 3anass ⊢ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
7 oveq1 ⊢ W = 2 → W − 1 = 2 − 1
8 2m1e1 ⊢ 2 − 1 = 1
9 7 8 eqtrdi ⊢ W = 2 → W − 1 = 1
10 9 oveq2d ⊢ W = 2 → 0 ..^ W − 1 = 0 ..^ 1
11 fzo01 ⊢ 0 ..^ 1 = 0
12 10 11 eqtrdi ⊢ W = 2 → 0 ..^ W − 1 = 0
13 12 adantr ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → 0 ..^ W − 1 = 0
14 13 raleqdv ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ ∀ i ∈ 0 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
15 c0ex ⊢ 0 ∈ V
16 fveq2 ⊢ i = 0 → W ⁡ i = W ⁡ 0
17 fv0p1e1 ⊢ i = 0 → W ⁡ i + 1 = W ⁡ 1
18 16 17 preq12d ⊢ i = 0 → W ⁡ i W ⁡ i + 1 = W ⁡ 0 W ⁡ 1
19 18 eleq1d ⊢ i = 0 → W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
20 15 19 ralsn ⊢ ∀ i ∈ 0 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
21 14 20 bitrdi ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
22 prcom ⊢ lastS ⁡ W W ⁡ 0 = W ⁡ 0 lastS ⁡ W
23 lsw ⊢ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ W − 1
24 9 fveq2d ⊢ W = 2 → W ⁡ W − 1 = W ⁡ 1
25 23 24 sylan9eqr ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ 1
26 25 preq2d ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → W ⁡ 0 lastS ⁡ W = W ⁡ 0 W ⁡ 1
27 22 26 syl5eq ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 = W ⁡ 0 W ⁡ 1
28 27 eleq1d ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
29 21 28 anbi12d ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
30 anidm ⊢ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
31 29 30 bitrdi ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
32 31 pm5.32da ⊢ W = 2 → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
33 6 32 syl5bb ⊢ W = 2 → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
34 33 pm5.32ri ⊢ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = 2 ↔ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ∧ W = 2
35 3anass ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ↔ W = 2 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
36 ancom ⊢ W = 2 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ↔ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ∧ W = 2
37 35 36 bitr2i ⊢ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G ∧ W = 2 ↔ W = 2 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G
38 5 34 37 3bitri ⊢ W ∈ 2 ClWWalksN G ↔ W = 2 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 W ⁡ 1 ∈ Edg ⁡ G