Theorem erclwwlkeq

Description: Two classes are equivalent regarding .~ if both are words and one is the other cyclically shifted. (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	erclwwlkeq	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑈 ∼ 𝑊 ↔ ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
2		eleq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ) )
3	2	adantr	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ) )
4		eleq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) )
5	4	adantl	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ) )
6		fveq2	⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
7	6	oveq2d	⊢ ( 𝑤 = 𝑊 → ( 0 ... ( ♯ ‘ 𝑤 ) ) = ( 0 ... ( ♯ ‘ 𝑊 ) ) )
8	7	adantl	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( 0 ... ( ♯ ‘ 𝑤 ) ) = ( 0 ... ( ♯ ‘ 𝑊 ) ) )
9		simpl	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → 𝑢 = 𝑈 )
10		oveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 cyclShift 𝑛 ) = ( 𝑊 cyclShift 𝑛 ) )
11	10	adantl	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( 𝑤 cyclShift 𝑛 ) = ( 𝑊 cyclShift 𝑛 ) )
12	9 11	eqeq12d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( 𝑢 = ( 𝑤 cyclShift 𝑛 ) ↔ 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) )
13	8 12	rexeqbidv	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) )
14	3 5 13	3anbi123d	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑤 = 𝑊 ) → ( ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) ↔ ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) ) )
15	14 1	brabga	⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑈 ∼ 𝑊 ↔ ( 𝑈 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) 𝑈 = ( 𝑊 cyclShift 𝑛 ) ) ) )