Metamath Proof Explorer

Theorem isclwwlknx

Description: Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v ⊢ V = Vtx ⁡ G
isclwwlknx.e ⊢ E = Edg ⁡ G
Assertion isclwwlknx ⊢ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N

Proof

Step Hyp Ref Expression
1 isclwwlknx.v ⊢ V = Vtx ⁡ G
2 isclwwlknx.e ⊢ E = Edg ⁡ G
3 eleq1 ⊢ W = N → W ∈ ℕ ↔ N ∈ ℕ
4 len0nnbi ⊢ W ∈ Word V → W ≠ ∅ ↔ W ∈ ℕ
5 4 biimprcd ⊢ W ∈ ℕ → W ∈ Word V → W ≠ ∅
6 3 5 biimtrrdi ⊢ W = N → N ∈ ℕ → W ∈ Word V → W ≠ ∅
7 6 impcom ⊢ N ∈ ℕ ∧ W = N → W ∈ Word V → W ≠ ∅
8 7 imp ⊢ N ∈ ℕ ∧ W = N ∧ W ∈ Word V → W ≠ ∅
9 8 biantrurd ⊢ N ∈ ℕ ∧ W = N ∧ W ∈ Word V → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
10 9 bicomd ⊢ N ∈ ℕ ∧ W = N ∧ W ∈ Word V → W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
11 10 pm5.32da ⊢ N ∈ ℕ ∧ W = N → W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
12 11 ex ⊢ N ∈ ℕ → W = N → W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
13 12 pm5.32rd ⊢ N ∈ ℕ → W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N
14 isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
15 1 2 isclwwlk ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
16 3anass ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
17 anass ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
18 16 17 bitri ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
19 15 18 bitri ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
20 19 anbi1i ⊢ W ∈ ClWWalks ⁡ G ∧ W = N ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N
21 14 20 bitri ⊢ W ∈ N ClWWalksN G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N
22 3anass ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
23 22 anbi1i ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N
24 13 21 23 3bitr4g ⊢ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N