Metamath Proof Explorer

Theorem clwwlkn1

Description: A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021) (Revised by AV, 11-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 2 3 isclwwlknx ⊢ 1 ∈ ℕ → W ∈ 1 ClWWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = 1
5 1 4 ax-mp ⊢ W ∈ 1 ClWWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = 1
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 ral0 ⊢ ∀ i ∈ ∅ W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
8 oveq1 ⊢ W = 1 → W − 1 = 1 − 1
9 1m1e0 ⊢ 1 − 1 = 0
10 8 9 eqtrdi ⊢ W = 1 → W − 1 = 0
11 10 oveq2d ⊢ W = 1 → 0 ..^ W − 1 = 0 ..^ 0
12 fzo0 ⊢ 0 ..^ 0 = ∅
13 11 12 eqtrdi ⊢ W = 1 → 0 ..^ W − 1 = ∅
14 13 raleqdv ⊢ W = 1 → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ ∀ i ∈ ∅ W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
15 14 adantr ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ↔ ∀ i ∈ ∅ W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
16 7 15 mpbiri ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
17 16 biantrurd ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
18 lsw1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → lastS ⁡ W = W ⁡ 0
19 18 ancoms ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W = W ⁡ 0
20 19 preq1d ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 = W ⁡ 0 W ⁡ 0
21 dfsn2 ⊢ W ⁡ 0 = W ⁡ 0 W ⁡ 0
22 20 21 eqtr4di ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 = W ⁡ 0
23 22 eleq1d ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ⁡ 0 ∈ Edg ⁡ G
24 17 23 bitr3d ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ⁡ 0 ∈ Edg ⁡ G
25 24 pm5.32da ⊢ W = 1 → 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 ∈ Edg ⁡ G
26 6 25 bitrid ⊢ W = 1 → 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 ∈ Edg ⁡ G
27 26 pm5.32ri ⊢ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = 1 ↔ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ∧ W = 1
28 3anass ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ↔ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G
29 ancom ⊢ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ↔ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ∧ W = 1
30 28 29 bitr2i ⊢ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G ∧ W = 1 ↔ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G
31 5 27 30 3bitri ⊢ W ∈ 1 ClWWalksN G ↔ W = 1 ∧ W ∈ Word Vtx ⁡ G ∧ W ⁡ 0 ∈ Edg ⁡ G