Metamath Proof Explorer

Theorem clwwlk1loop

Description: A closed walk of length 1 is a loop. See also clwlkl1loop . (Contributed by AV, 24-Apr-2021)

Ref Expression
Assertion clwwlk1loop ⊢ W ∈ ClWWalks ⁡ G ∧ W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 isclwwlk ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
4 lsw1 ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → lastS ⁡ W = W ⁡ 0
5 4 preq1d ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → lastS ⁡ W W ⁡ 0 = W ⁡ 0 W ⁡ 0
6 5 eleq1d ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ↔ W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
7 6 biimpd ⊢ W ∈ Word Vtx ⁡ G ∧ W = 1 → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
8 7 ex ⊢ W ∈ Word Vtx ⁡ G → W = 1 → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
9 8 com23 ⊢ W ∈ Word Vtx ⁡ G → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
10 9 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
11 10 imp ⊢ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
12 11 3adant2 ⊢ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
13 3 12 sylbi ⊢ W ∈ ClWWalks ⁡ G → W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G
14 13 imp ⊢ W ∈ ClWWalks ⁡ G ∧ W = 1 → W ⁡ 0 W ⁡ 0 ∈ Edg ⁡ G