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 ⊢ ∼ ˙ = u w | u ∈ ClWWalks ⁡ G ∧ w ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … w u = w cyclShift n
Assertion erclwwlkeq ⊢ U ∈ X ∧ W ∈ Y → U ∼ ˙ W ↔ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … W U = W cyclShift n

Proof

Step Hyp Ref Expression
1 erclwwlk.r ⊢ ∼ ˙ = u w | u ∈ ClWWalks ⁡ G ∧ w ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … w u = w cyclShift n
2 eleq1 ⊢ u = U → u ∈ ClWWalks ⁡ G ↔ U ∈ ClWWalks ⁡ G
3 2 adantr ⊢ u = U ∧ w = W → u ∈ ClWWalks ⁡ G ↔ U ∈ ClWWalks ⁡ G
4 eleq1 ⊢ w = W → w ∈ ClWWalks ⁡ G ↔ W ∈ ClWWalks ⁡ G
5 4 adantl ⊢ u = U ∧ w = W → w ∈ ClWWalks ⁡ G ↔ W ∈ ClWWalks ⁡ G
6 fveq2 ⊢ w = W → w = W
7 6 oveq2d ⊢ w = W → 0 … w = 0 … W
8 7 adantl ⊢ u = U ∧ w = W → 0 … w = 0 … W
9 simpl ⊢ u = U ∧ w = W → u = U
10 oveq1 ⊢ w = W → w cyclShift n = W cyclShift n
11 10 adantl ⊢ u = U ∧ w = W → w cyclShift n = W cyclShift n
12 9 11 eqeq12d ⊢ u = U ∧ w = W → u = w cyclShift n ↔ U = W cyclShift n
13 8 12 rexeqbidv ⊢ u = U ∧ w = W → ∃ n ∈ 0 … w u = w cyclShift n ↔ ∃ n ∈ 0 … W U = W cyclShift n
14 3 5 13 3anbi123d ⊢ u = U ∧ w = W → u ∈ ClWWalks ⁡ G ∧ w ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … w u = w cyclShift n ↔ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … W U = W cyclShift n
15 14 1 brabga ⊢ U ∈ X ∧ W ∈ Y → U ∼ ˙ W ↔ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … W U = W cyclShift n