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

Proof

Step Hyp Ref Expression
1 erclwwlk.r ⊢∼˙=uw|u∈ClWWalks⁡G∧w∈ClWWalks⁡G∧∃n∈0…wu=wcyclShiftn
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→wcyclShiftn=WcyclShiftn
11 10 adantl ⊢u=U∧w=W→wcyclShiftn=WcyclShiftn
12 9 11 eqeq12d ⊢u=U∧w=W→u=wcyclShiftn↔U=WcyclShiftn
13 8 12 rexeqbidv ⊢u=U∧w=W→∃n∈0…wu=wcyclShiftn↔∃n∈0…WU=WcyclShiftn
14 3 5 13 3anbi123d ⊢u=U∧w=W→u∈ClWWalks⁡G∧w∈ClWWalks⁡G∧∃n∈0…wu=wcyclShiftn↔U∈ClWWalks⁡G∧W∈ClWWalks⁡G∧∃n∈0…WU=WcyclShiftn
15 14 1 brabga ⊢U∈X∧W∈Y→U∼˙W↔U∈ClWWalks⁡G∧W∈ClWWalks⁡G∧∃n∈0…WU=WcyclShiftn