Metamath Proof Explorer


Theorem clwwlknscsh

Description: The set of cyclical shifts of a word representing a closed walk is the set of closed walks represented by cyclical shifts of a word. (Contributed by Alexander van der Vekens, 15-Jun-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Assertion clwwlknscsh N 0 W N ClWWalksN G y N ClWWalksN G | n 0 N y = W cyclShift n = y Word Vtx G | n 0 N y = W cyclShift n

Proof

Step Hyp Ref Expression
1 eqeq1 y = x y = W cyclShift n x = W cyclShift n
2 1 rexbidv y = x n 0 N y = W cyclShift n n 0 N x = W cyclShift n
3 2 cbvrabv y N ClWWalksN G | n 0 N y = W cyclShift n = x N ClWWalksN G | n 0 N x = W cyclShift n
4 eqid Vtx G = Vtx G
5 4 clwwlknwrd w N ClWWalksN G w Word Vtx G
6 5 ad2antrl N 0 W N ClWWalksN G w N ClWWalksN G n 0 N w = W cyclShift n w Word Vtx G
7 simprr N 0 W N ClWWalksN G w N ClWWalksN G n 0 N w = W cyclShift n n 0 N w = W cyclShift n
8 6 7 jca N 0 W N ClWWalksN G w N ClWWalksN G n 0 N w = W cyclShift n w Word Vtx G n 0 N w = W cyclShift n
9 simprr w Word Vtx G n 0 N N 0 W N ClWWalksN G W N ClWWalksN G
10 simpllr w Word Vtx G n 0 N N 0 W N ClWWalksN G w = W cyclShift n n 0 N
11 clwwnisshclwwsn W N ClWWalksN G n 0 N W cyclShift n N ClWWalksN G
12 9 10 11 syl2an2r w Word Vtx G n 0 N N 0 W N ClWWalksN G w = W cyclShift n W cyclShift n N ClWWalksN G
13 eleq1 w = W cyclShift n w N ClWWalksN G W cyclShift n N ClWWalksN G
14 13 adantl w Word Vtx G n 0 N N 0 W N ClWWalksN G w = W cyclShift n w N ClWWalksN G W cyclShift n N ClWWalksN G
15 12 14 mpbird w Word Vtx G n 0 N N 0 W N ClWWalksN G w = W cyclShift n w N ClWWalksN G
16 15 exp31 w Word Vtx G n 0 N N 0 W N ClWWalksN G w = W cyclShift n w N ClWWalksN G
17 16 com23 w Word Vtx G n 0 N w = W cyclShift n N 0 W N ClWWalksN G w N ClWWalksN G
18 17 rexlimdva w Word Vtx G n 0 N w = W cyclShift n N 0 W N ClWWalksN G w N ClWWalksN G
19 18 imp w Word Vtx G n 0 N w = W cyclShift n N 0 W N ClWWalksN G w N ClWWalksN G
20 19 impcom N 0 W N ClWWalksN G w Word Vtx G n 0 N w = W cyclShift n w N ClWWalksN G
21 simprr N 0 W N ClWWalksN G w Word Vtx G n 0 N w = W cyclShift n n 0 N w = W cyclShift n
22 20 21 jca N 0 W N ClWWalksN G w Word Vtx G n 0 N w = W cyclShift n w N ClWWalksN G n 0 N w = W cyclShift n
23 8 22 impbida N 0 W N ClWWalksN G w N ClWWalksN G n 0 N w = W cyclShift n w Word Vtx G n 0 N w = W cyclShift n
24 eqeq1 x = w x = W cyclShift n w = W cyclShift n
25 24 rexbidv x = w n 0 N x = W cyclShift n n 0 N w = W cyclShift n
26 25 elrab w x N ClWWalksN G | n 0 N x = W cyclShift n w N ClWWalksN G n 0 N w = W cyclShift n
27 eqeq1 y = w y = W cyclShift n w = W cyclShift n
28 27 rexbidv y = w n 0 N y = W cyclShift n n 0 N w = W cyclShift n
29 28 elrab w y Word Vtx G | n 0 N y = W cyclShift n w Word Vtx G n 0 N w = W cyclShift n
30 23 26 29 3bitr4g N 0 W N ClWWalksN G w x N ClWWalksN G | n 0 N x = W cyclShift n w y Word Vtx G | n 0 N y = W cyclShift n
31 30 eqrdv N 0 W N ClWWalksN G x N ClWWalksN G | n 0 N x = W cyclShift n = y Word Vtx G | n 0 N y = W cyclShift n
32 3 31 eqtrid N 0 W N ClWWalksN G y N ClWWalksN G | n 0 N y = W cyclShift n = y Word Vtx G | n 0 N y = W cyclShift n