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 e. NN0 /\ W e. ( N ClWWalksN G ) ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 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 -> ( E. n e. ( 0 ... N ) y = ( W cyclShift n ) <-> E. n e. ( 0 ... N ) x = ( W cyclShift n ) ) )
3 2 cbvrabv
 |-  { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } = { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) }
4 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 clwwlknwrd
 |-  ( w e. ( N ClWWalksN G ) -> w e. Word ( Vtx ` G ) )
6 5 ad2antrl
 |-  ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> w e. Word ( Vtx ` G ) )
7 simprr
 |-  ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> E. n e. ( 0 ... N ) w = ( W cyclShift n ) )
8 6 7 jca
 |-  ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) )
9 simprr
 |-  ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) -> W e. ( N ClWWalksN G ) )
10 simpllr
 |-  ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> n e. ( 0 ... N ) )
11 clwwnisshclwwsn
 |-  ( ( W e. ( N ClWWalksN G ) /\ n e. ( 0 ... N ) ) -> ( W cyclShift n ) e. ( N ClWWalksN G ) )
12 9 10 11 syl2an2r
 |-  ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> ( W cyclShift n ) e. ( N ClWWalksN G ) )
13 eleq1
 |-  ( w = ( W cyclShift n ) -> ( w e. ( N ClWWalksN G ) <-> ( W cyclShift n ) e. ( N ClWWalksN G ) ) )
14 13 adantl
 |-  ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> ( w e. ( N ClWWalksN G ) <-> ( W cyclShift n ) e. ( N ClWWalksN G ) ) )
15 12 14 mpbird
 |-  ( ( ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) /\ ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) ) /\ w = ( W cyclShift n ) ) -> w e. ( N ClWWalksN G ) )
16 15 exp31
 |-  ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> ( w = ( W cyclShift n ) -> w e. ( N ClWWalksN G ) ) ) )
17 16 com23
 |-  ( ( w e. Word ( Vtx ` G ) /\ n e. ( 0 ... N ) ) -> ( w = ( W cyclShift n ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> w e. ( N ClWWalksN G ) ) ) )
18 17 rexlimdva
 |-  ( w e. Word ( Vtx ` G ) -> ( E. n e. ( 0 ... N ) w = ( W cyclShift n ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> w e. ( N ClWWalksN G ) ) ) )
19 18 imp
 |-  ( ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) -> ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> w e. ( N ClWWalksN G ) ) )
20 19 impcom
 |-  ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> w e. ( N ClWWalksN G ) )
21 simprr
 |-  ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> E. n e. ( 0 ... N ) w = ( W cyclShift n ) )
22 20 21 jca
 |-  ( ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) /\ ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) -> ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) )
23 8 22 impbida
 |-  ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> ( ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) <-> ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) ) )
24 eqeq1
 |-  ( x = w -> ( x = ( W cyclShift n ) <-> w = ( W cyclShift n ) ) )
25 24 rexbidv
 |-  ( x = w -> ( E. n e. ( 0 ... N ) x = ( W cyclShift n ) <-> E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) )
26 25 elrab
 |-  ( w e. { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } <-> ( w e. ( N ClWWalksN G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) )
27 eqeq1
 |-  ( y = w -> ( y = ( W cyclShift n ) <-> w = ( W cyclShift n ) ) )
28 27 rexbidv
 |-  ( y = w -> ( E. n e. ( 0 ... N ) y = ( W cyclShift n ) <-> E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) )
29 28 elrab
 |-  ( w e. { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } <-> ( w e. Word ( Vtx ` G ) /\ E. n e. ( 0 ... N ) w = ( W cyclShift n ) ) )
30 23 26 29 3bitr4g
 |-  ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> ( w e. { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } <-> w e. { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } ) )
31 30 eqrdv
 |-  ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> { x e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) x = ( W cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } )
32 3 31 syl5eq
 |-  ( ( N e. NN0 /\ W e. ( N ClWWalksN G ) ) -> { y e. ( N ClWWalksN G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } = { y e. Word ( Vtx ` G ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } )