Metamath Proof Explorer


Theorem eclclwwlkn1

Description: An equivalence class according to .~ . (Contributed by Alexander van der Vekens, 12-Apr-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypotheses erclwwlkn.w W = N ClWWalksN G
erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
Assertion eclclwwlkn1 B X B W / ˙ x W B = y W | n 0 N y = x cyclShift n

Proof

Step Hyp Ref Expression
1 erclwwlkn.w W = N ClWWalksN G
2 erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
3 elqsecl B X B W / ˙ x W B = y | x ˙ y
4 1 2 erclwwlknsym x ˙ y y ˙ x
5 1 2 erclwwlknsym y ˙ x x ˙ y
6 4 5 impbii x ˙ y y ˙ x
7 6 a1i B X x W x ˙ y y ˙ x
8 7 abbidv B X x W y | x ˙ y = y | y ˙ x
9 1 2 erclwwlkneq y V x V y ˙ x y W x W n 0 N y = x cyclShift n
10 9 el2v y ˙ x y W x W n 0 N y = x cyclShift n
11 10 a1i B X x W y ˙ x y W x W n 0 N y = x cyclShift n
12 11 abbidv B X x W y | y ˙ x = y | y W x W n 0 N y = x cyclShift n
13 3anan12 y W x W n 0 N y = x cyclShift n x W y W n 0 N y = x cyclShift n
14 ibar x W y W n 0 N y = x cyclShift n x W y W n 0 N y = x cyclShift n
15 14 bicomd x W x W y W n 0 N y = x cyclShift n y W n 0 N y = x cyclShift n
16 15 adantl B X x W x W y W n 0 N y = x cyclShift n y W n 0 N y = x cyclShift n
17 13 16 syl5bb B X x W y W x W n 0 N y = x cyclShift n y W n 0 N y = x cyclShift n
18 17 abbidv B X x W y | y W x W n 0 N y = x cyclShift n = y | y W n 0 N y = x cyclShift n
19 df-rab y W | n 0 N y = x cyclShift n = y | y W n 0 N y = x cyclShift n
20 18 19 eqtr4di B X x W y | y W x W n 0 N y = x cyclShift n = y W | n 0 N y = x cyclShift n
21 8 12 20 3eqtrd B X x W y | x ˙ y = y W | n 0 N y = x cyclShift n
22 21 eqeq2d B X x W B = y | x ˙ y B = y W | n 0 N y = x cyclShift n
23 22 rexbidva B X x W B = y | x ˙ y x W B = y W | n 0 N y = x cyclShift n
24 3 23 bitrd B X B W / ˙ x W B = y W | n 0 N y = x cyclShift n