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 ‘ 𝐺 ) ↔ 𝑥 𝑥 )