This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erclwwlknref

Description: .~ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018) (Revised by AV, 30-Apr-2021) (Proof shortened by AV, 23-Mar-2022)

Ref Expression
Hypotheses erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion erclwwlknref ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥 )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 df-3an ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
4 anidm ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ↔ 𝑥 ∈ 𝑊 )
5 4 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ) ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
6 3 5 bitri ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
7 1 2 erclwwlkneq ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ) )
8 7 el2v ⊢ ( 𝑥 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
9 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 9 clwwlknwrd ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) )
11 clwwlknnn ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 ∈ ℕ )
12 cshw0 ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑥 cyclShift 0 ) = 𝑥 )
13 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
14 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
15 13 14 syl ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ( 0 ... 𝑁 ) )
16 eqcom ⊢ ( ( 𝑥 cyclShift 0 ) = 𝑥 ↔ 𝑥 = ( 𝑥 cyclShift 0 ) )
17 16 biimpi ⊢ ( ( 𝑥 cyclShift 0 ) = 𝑥 → 𝑥 = ( 𝑥 cyclShift 0 ) )
18 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 0 ) )
19 18 rspceeqv ⊢ ( ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑥 cyclShift 0 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
20 15 17 19 syl2anr ⊢ ( ( ( 𝑥 cyclShift 0 ) = 𝑥 ∧ 𝑁 ∈ ℕ ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
21 20 ex ⊢ ( ( 𝑥 cyclShift 0 ) = 𝑥 → ( 𝑁 ∈ ℕ → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
22 12 21 syl ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑁 ∈ ℕ → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
23 10 11 22 sylc ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
24 23 1 eleq2s ⊢ ( 𝑥 ∈ 𝑊 → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
25 24 pm4.71i ⊢ ( 𝑥 ∈ 𝑊 ↔ ( 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
26 6 8 25 3bitr4ri ⊢ ( 𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥 )