Metamath Proof Explorer

Theorem loopclwwlkn1b

Description: The singleton word consisting of a vertex V represents a closed walk of length 1 iff there is a loop at vertex V . (Contributed by AV, 11-Feb-2022)

Ref Expression
Assertion loopclwwlkn1b ⊢ V ∈ Vtx ⁡ G → V ∈ Edg ⁡ G ↔ ⟨“ V ”⟩ ∈ 1 ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlkn1 ⊢ ⟨“ V ”⟩ ∈ 1 ClWWalksN G ↔ ⟨“ V ”⟩ = 1 ∧ ⟨“ V ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G
2 s1fv ⊢ V ∈ Vtx ⁡ G → ⟨“ V ”⟩ ⁡ 0 = V
3 2 sneqd ⊢ V ∈ Vtx ⁡ G → ⟨“ V ”⟩ ⁡ 0 = V
4 3 eleq1d ⊢ V ∈ Vtx ⁡ G → ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G ↔ V ∈ Edg ⁡ G
5 4 biimpcd ⊢ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G → V ∈ Vtx ⁡ G → V ∈ Edg ⁡ G
6 5 3ad2ant3 ⊢ ⟨“ V ”⟩ = 1 ∧ ⟨“ V ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G → V ∈ Vtx ⁡ G → V ∈ Edg ⁡ G
7 6 com12 ⊢ V ∈ Vtx ⁡ G → ⟨“ V ”⟩ = 1 ∧ ⟨“ V ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G → V ∈ Edg ⁡ G
8 s1len ⊢ ⟨“ V ”⟩ = 1
9 8 a1i ⊢ V ∈ Vtx ⁡ G ∧ V ∈ Edg ⁡ G → ⟨“ V ”⟩ = 1
10 s1cl ⊢ V ∈ Vtx ⁡ G → ⟨“ V ”⟩ ∈ Word Vtx ⁡ G
11 10 adantr ⊢ V ∈ Vtx ⁡ G ∧ V ∈ Edg ⁡ G → ⟨“ V ”⟩ ∈ Word Vtx ⁡ G
12 2 eqcomd ⊢ V ∈ Vtx ⁡ G → V = ⟨“ V ”⟩ ⁡ 0
13 12 sneqd ⊢ V ∈ Vtx ⁡ G → V = ⟨“ V ”⟩ ⁡ 0
14 13 eleq1d ⊢ V ∈ Vtx ⁡ G → V ∈ Edg ⁡ G ↔ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G
15 14 biimpa ⊢ V ∈ Vtx ⁡ G ∧ V ∈ Edg ⁡ G → ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G
16 9 11 15 3jca ⊢ V ∈ Vtx ⁡ G ∧ V ∈ Edg ⁡ G → ⟨“ V ”⟩ = 1 ∧ ⟨“ V ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G
17 16 ex ⊢ V ∈ Vtx ⁡ G → V ∈ Edg ⁡ G → ⟨“ V ”⟩ = 1 ∧ ⟨“ V ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G
18 7 17 impbid ⊢ V ∈ Vtx ⁡ G → ⟨“ V ”⟩ = 1 ∧ ⟨“ V ”⟩ ∈ Word Vtx ⁡ G ∧ ⟨“ V ”⟩ ⁡ 0 ∈ Edg ⁡ G ↔ V ∈ Edg ⁡ G
19 1 18 bitr2id ⊢ V ∈ Vtx ⁡ G → V ∈ Edg ⁡ G ↔ ⟨“ V ”⟩ ∈ 1 ClWWalksN G