Metamath Proof Explorer

Theorem erclwwlkeqlen

Description: If two classes are equivalent regarding .~ , then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-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 erclwwlkeqlen ⊢ U ∈ X ∧ W ∈ Y → U ∼ ˙ W → U = W

Proof

Step Hyp Ref Expression
1 erclwwlk.r ⊢ ∼ ˙ = u w | u ∈ ClWWalks ⁡ G ∧ w ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … w u = w cyclShift n
2 1 erclwwlkeq ⊢ U ∈ X ∧ W ∈ Y → U ∼ ˙ W ↔ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … W U = W cyclShift n
3 fveq2 ⊢ U = W cyclShift n → U = W cyclShift n
4 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
5 4 clwwlkbp ⊢ W ∈ ClWWalks ⁡ G → G ∈ V ∧ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅
6 5 simp2d ⊢ W ∈ ClWWalks ⁡ G → W ∈ Word Vtx ⁡ G
7 6 ad2antlr ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ U ∈ X ∧ W ∈ Y → W ∈ Word Vtx ⁡ G
8 elfzelz ⊢ n ∈ 0 … W → n ∈ ℤ
9 cshwlen ⊢ W ∈ Word Vtx ⁡ G ∧ n ∈ ℤ → W cyclShift n = W
10 7 8 9 syl2an ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ U ∈ X ∧ W ∈ Y ∧ n ∈ 0 … W → W cyclShift n = W
11 3 10 sylan9eqr ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ U ∈ X ∧ W ∈ Y ∧ n ∈ 0 … W ∧ U = W cyclShift n → U = W
12 11 rexlimdva2 ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ U ∈ X ∧ W ∈ Y → ∃ n ∈ 0 … W U = W cyclShift n → U = W
13 12 ex ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G → U ∈ X ∧ W ∈ Y → ∃ n ∈ 0 … W U = W cyclShift n → U = W
14 13 com23 ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G → ∃ n ∈ 0 … W U = W cyclShift n → U ∈ X ∧ W ∈ Y → U = W
15 14 3impia ⊢ U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … W U = W cyclShift n → U ∈ X ∧ W ∈ Y → U = W
16 15 com12 ⊢ U ∈ X ∧ W ∈ Y → U ∈ ClWWalks ⁡ G ∧ W ∈ ClWWalks ⁡ G ∧ ∃ n ∈ 0 … W U = W cyclShift n → U = W
17 2 16 sylbid ⊢ U ∈ X ∧ W ∈ Y → U ∼ ˙ W → U = W