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

Metamath Proof Explorer

Theorem erclwwlkref

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

Ref Expression
Hypothesis erclwwlk.r ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
Assertion erclwwlkref ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑥 ∼ 𝑥 )

Proof

Step Hyp Ref Expression
1 erclwwlk.r ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
2 anidm ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ) ↔ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) )
3 2 anbi1i ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
4 df-3an ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ↔ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
5 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6 5 clwwlkbp ⊢ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ) )
7 cshw0 ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( 𝑥 cyclShift 0 ) = 𝑥 )
8 0nn0 ⊢ 0 ∈ ℕ0
9 8 a1i ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → 0 ∈ ℕ0 )
10 lencl ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑥 ) ∈ ℕ0 )
11 hashge0 ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → 0 ≤ ( ♯ ‘ 𝑥 ) )
12 elfz2nn0 ⊢ ( 0 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ↔ ( 0 ∈ ℕ0 ∧ ( ♯ ‘ 𝑥 ) ∈ ℕ0 ∧ 0 ≤ ( ♯ ‘ 𝑥 ) ) )
13 9 10 11 12 syl3anbrc ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → 0 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) )
14 eqcom ⊢ ( ( 𝑥 cyclShift 0 ) = 𝑥 ↔ 𝑥 = ( 𝑥 cyclShift 0 ) )
15 14 biimpi ⊢ ( ( 𝑥 cyclShift 0 ) = 𝑥 → 𝑥 = ( 𝑥 cyclShift 0 ) )
16 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 0 ) )
17 16 rspceeqv ⊢ ( ( 0 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ 𝑥 = ( 𝑥 cyclShift 0 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
18 13 15 17 syl2an ⊢ ( ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( 𝑥 cyclShift 0 ) = 𝑥 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
19 7 18 mpdan ⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
20 19 3ad2ant2 ⊢ ( ( 𝐺 ∈ V ∧ 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
21 6 20 syl ⊢ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) )
22 21 pm4.71i ⊢ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
23 3 4 22 3bitr4ri ⊢ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
24 1 erclwwlkeq ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∼ 𝑥 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) ) )
25 24 el2v ⊢ ( 𝑥 ∼ 𝑥 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑥 = ( 𝑥 cyclShift 𝑛 ) ) )
26 23 25 bitr4i ⊢ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑥 ∼ 𝑥 )