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 ) } )