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 ( 𝑥𝑊𝑥 𝑥 )