Metamath Proof Explorer

Theorem clwwlk

Description: The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Hypotheses clwwlk.v ⊢ V = Vtx ⁡ G
clwwlk.e ⊢ E = Edg ⁡ G
Assertion clwwlk ⊢ ClWWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E

Proof

Step Hyp Ref Expression
1 clwwlk.v ⊢ V = Vtx ⁡ G
2 clwwlk.e ⊢ E = Edg ⁡ G
3 df-clwwlk ⊢ ClWWalks = g ∈ V ⟼ w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g
4 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
5 4 1 eqtr4di ⊢ g = G → Vtx ⁡ g = V
6 wrdeq ⊢ Vtx ⁡ g = V → Word Vtx ⁡ g = Word V
7 5 6 syl ⊢ g = G → Word Vtx ⁡ g = Word V
8 fveq2 ⊢ g = G → Edg ⁡ g = Edg ⁡ G
9 8 2 eqtr4di ⊢ g = G → Edg ⁡ g = E
10 9 eleq2d ⊢ g = G → w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ↔ w ⁡ i w ⁡ i + 1 ∈ E
11 10 ralbidv ⊢ g = G → ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ↔ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E
12 9 eleq2d ⊢ g = G → lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g ↔ lastS ⁡ w w ⁡ 0 ∈ E
13 11 12 3anbi23d ⊢ g = G → w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g ↔ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
14 7 13 rabeqbidv ⊢ g = G → w ∈ Word Vtx ⁡ g | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ Edg ⁡ g ∧ lastS ⁡ w w ⁡ 0 ∈ Edg ⁡ g = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
15 id ⊢ G ∈ V → G ∈ V
16 1 fvexi ⊢ V ∈ V
17 16 a1i ⊢ G ∈ V → V ∈ V
18 wrdexg ⊢ V ∈ V → Word V ∈ V
19 rabexg ⊢ Word V ∈ V → w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E ∈ V
20 17 18 19 3syl ⊢ G ∈ V → w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E ∈ V
21 3 14 15 20 fvmptd3 ⊢ G ∈ V → ClWWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
22 fvprc ⊢ ¬ G ∈ V → ClWWalks ⁡ G = ∅
23 noel ⊢ ¬ lastS ⁡ w w ⁡ 0 ∈ ∅
24 fvprc ⊢ ¬ G ∈ V → Edg ⁡ G = ∅
25 2 24 syl5eq ⊢ ¬ G ∈ V → E = ∅
26 25 eleq2d ⊢ ¬ G ∈ V → lastS ⁡ w w ⁡ 0 ∈ E ↔ lastS ⁡ w w ⁡ 0 ∈ ∅
27 23 26 mtbiri ⊢ ¬ G ∈ V → ¬ lastS ⁡ w w ⁡ 0 ∈ E
28 27 adantr ⊢ ¬ G ∈ V ∧ w ∈ Word V → ¬ lastS ⁡ w w ⁡ 0 ∈ E
29 28 intn3an3d ⊢ ¬ G ∈ V ∧ w ∈ Word V → ¬ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
30 29 ralrimiva ⊢ ¬ G ∈ V → ∀ w ∈ Word V ¬ w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
31 rabeq0 ⊢ 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
32 30 31 sylibr ⊢ ¬ G ∈ V → w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E = ∅
33 22 32 eqtr4d ⊢ ¬ G ∈ V → ClWWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E
34 21 33 pm2.61i ⊢ ClWWalks ⁡ G = w ∈ Word V | w ≠ ∅ ∧ ∀ i ∈ 0 ..^ w − 1 w ⁡ i w ⁡ i + 1 ∈ E ∧ lastS ⁡ w w ⁡ 0 ∈ E