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