Metamath Proof Explorer

Theorem clwwlknon1

Description: The set of closed walks on vertex X of length 1 in a graph G as words over the set of vertices. (Contributed by AV, 11-Feb-2022) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 24-Mar-2022)

Ref Expression
Hypotheses clwwlknon1.v ⊢ V = Vtx ⁡ G
clwwlknon1.c ⊢ C = ClWWalksNOn ⁡ G
clwwlknon1.e ⊢ E = Edg ⁡ G
Assertion clwwlknon1 ⊢ X ∈ V → X C 1 = w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E

Proof

Step Hyp Ref Expression
1 clwwlknon1.v ⊢ V = Vtx ⁡ G
2 clwwlknon1.c ⊢ C = ClWWalksNOn ⁡ G
3 clwwlknon1.e ⊢ E = Edg ⁡ G
4 2 oveqi ⊢ X C 1 = X ClWWalksNOn ⁡ G 1
5 4 a1i ⊢ X ∈ V → X C 1 = X ClWWalksNOn ⁡ G 1
6 clwwlknon ⊢ X ClWWalksNOn ⁡ G 1 = w ∈ 1 ClWWalksN G | w ⁡ 0 = X
7 6 a1i ⊢ X ∈ V → X ClWWalksNOn ⁡ G 1 = w ∈ 1 ClWWalksN G | w ⁡ 0 = X
8 clwwlkn1 ⊢ w ∈ 1 ClWWalksN G ↔ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G
9 8 anbi1i ⊢ w ∈ 1 ClWWalksN G ∧ w ⁡ 0 = X ↔ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
10 1 eqcomi ⊢ Vtx ⁡ G = V
11 10 wrdeqi ⊢ Word Vtx ⁡ G = Word V
12 11 eleq2i ⊢ w ∈ Word Vtx ⁡ G ↔ w ∈ Word V
13 12 biimpi ⊢ w ∈ Word Vtx ⁡ G → w ∈ Word V
14 13 3ad2ant2 ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G → w ∈ Word V
15 14 ad2antrl ⊢ X ∈ V ∧ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w ∈ Word V
16 14 adantr ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w ∈ Word V
17 simpl1 ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w = 1
18 simpr ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w ⁡ 0 = X
19 16 17 18 3jca ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w ∈ Word V ∧ w = 1 ∧ w ⁡ 0 = X
20 19 adantl ⊢ X ∈ V ∧ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w ∈ Word V ∧ w = 1 ∧ w ⁡ 0 = X
21 wrdl1s1 ⊢ X ∈ V → w = ⟨“ X ”⟩ ↔ w ∈ Word V ∧ w = 1 ∧ w ⁡ 0 = X
22 21 adantr ⊢ X ∈ V ∧ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w = ⟨“ X ”⟩ ↔ w ∈ Word V ∧ w = 1 ∧ w ⁡ 0 = X
23 20 22 mpbird ⊢ X ∈ V ∧ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w = ⟨“ X ”⟩
24 sneq ⊢ w ⁡ 0 = X → w ⁡ 0 = X
25 3 eqcomi ⊢ Edg ⁡ G = E
26 25 a1i ⊢ w ⁡ 0 = X → Edg ⁡ G = E
27 24 26 eleq12d ⊢ w ⁡ 0 = X → w ⁡ 0 ∈ Edg ⁡ G ↔ X ∈ E
28 27 biimpd ⊢ w ⁡ 0 = X → w ⁡ 0 ∈ Edg ⁡ G → X ∈ E
29 28 a1i ⊢ X ∈ V → w ⁡ 0 = X → w ⁡ 0 ∈ Edg ⁡ G → X ∈ E
30 29 com13 ⊢ w ⁡ 0 ∈ Edg ⁡ G → w ⁡ 0 = X → X ∈ V → X ∈ E
31 30 3ad2ant3 ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G → w ⁡ 0 = X → X ∈ V → X ∈ E
32 31 imp ⊢ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → X ∈ V → X ∈ E
33 32 impcom ⊢ X ∈ V ∧ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → X ∈ E
34 15 23 33 jca32 ⊢ X ∈ V ∧ w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X → w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E
35 fveq2 ⊢ w = ⟨“ X ”⟩ → w = ⟨“ X ”⟩
36 s1len ⊢ ⟨“ X ”⟩ = 1
37 35 36 eqtrdi ⊢ w = ⟨“ X ”⟩ → w = 1
38 37 ad2antrl ⊢ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w = 1
39 38 adantl ⊢ X ∈ V ∧ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w = 1
40 1 wrdeqi ⊢ Word V = Word Vtx ⁡ G
41 40 eleq2i ⊢ w ∈ Word V ↔ w ∈ Word Vtx ⁡ G
42 41 biimpi ⊢ w ∈ Word V → w ∈ Word Vtx ⁡ G
43 42 ad2antrl ⊢ X ∈ V ∧ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w ∈ Word Vtx ⁡ G
44 fveq1 ⊢ w = ⟨“ X ”⟩ → w ⁡ 0 = ⟨“ X ”⟩ ⁡ 0
45 s1fv ⊢ X ∈ V → ⟨“ X ”⟩ ⁡ 0 = X
46 44 45 sylan9eq ⊢ w = ⟨“ X ”⟩ ∧ X ∈ V → w ⁡ 0 = X
47 46 eqcomd ⊢ w = ⟨“ X ”⟩ ∧ X ∈ V → X = w ⁡ 0
48 47 sneqd ⊢ w = ⟨“ X ”⟩ ∧ X ∈ V → X = w ⁡ 0
49 3 a1i ⊢ w = ⟨“ X ”⟩ ∧ X ∈ V → E = Edg ⁡ G
50 48 49 eleq12d ⊢ w = ⟨“ X ”⟩ ∧ X ∈ V → X ∈ E ↔ w ⁡ 0 ∈ Edg ⁡ G
51 50 biimpd ⊢ w = ⟨“ X ”⟩ ∧ X ∈ V → X ∈ E → w ⁡ 0 ∈ Edg ⁡ G
52 51 impancom ⊢ w = ⟨“ X ”⟩ ∧ X ∈ E → X ∈ V → w ⁡ 0 ∈ Edg ⁡ G
53 52 adantl ⊢ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → X ∈ V → w ⁡ 0 ∈ Edg ⁡ G
54 53 impcom ⊢ X ∈ V ∧ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w ⁡ 0 ∈ Edg ⁡ G
55 39 43 54 3jca ⊢ X ∈ V ∧ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G
56 46 ex ⊢ w = ⟨“ X ”⟩ → X ∈ V → w ⁡ 0 = X
57 56 ad2antrl ⊢ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → X ∈ V → w ⁡ 0 = X
58 57 impcom ⊢ X ∈ V ∧ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w ⁡ 0 = X
59 55 58 jca ⊢ X ∈ V ∧ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E → w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
60 34 59 impbida ⊢ X ∈ V → w = 1 ∧ w ∈ Word Vtx ⁡ G ∧ w ⁡ 0 ∈ Edg ⁡ G ∧ w ⁡ 0 = X ↔ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E
61 9 60 syl5bb ⊢ X ∈ V → w ∈ 1 ClWWalksN G ∧ w ⁡ 0 = X ↔ w ∈ Word V ∧ w = ⟨“ X ”⟩ ∧ X ∈ E
62 61 rabbidva2 ⊢ X ∈ V → w ∈ 1 ClWWalksN G | w ⁡ 0 = X = w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E
63 5 7 62 3eqtrd ⊢ X ∈ V → X C 1 = w ∈ Word V | w = ⟨“ X ”⟩ ∧ X ∈ E