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 ∈ ℕ₀
9	8	a1i	⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → 0 ∈ ℕ₀ )
10		lencl	⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑥 ) ∈ ℕ₀ )
11		hashge0	⊢ ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) → 0 ≤ ( ♯ ‘ 𝑥 ) )
12		elfz2nn0	⊢ ( 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 ‘ 𝐺 ) ↔ 𝑥 ∼ 𝑥 )

Metamath Proof Explorer

Theorem erclwwlkref

Proof