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

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