Metamath Proof Explorer


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 𝑛 ) ) ) )