This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwisshclwwsn

Description: Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jun-2018) (Revised by AV, 29-Apr-2021)

Ref Expression
Assertion clwwisshclwwsn 
|- ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( N = ( # ` W ) -> ( W cyclShift N ) = ( W cyclShift ( # ` W ) ) )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 clwwlkbp 
 |-  ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word ( Vtx ` G ) /\ W =/= (/) ) )
4 3 simp2d 
 |-  ( W e. ( ClWWalks ` G ) -> W e. Word ( Vtx ` G ) )
5 cshwn 
 |-  ( W e. Word ( Vtx ` G ) -> ( W cyclShift ( # ` W ) ) = W )
6 4 5 syl 
 |-  ( W e. ( ClWWalks ` G ) -> ( W cyclShift ( # ` W ) ) = W )
7 6 adantr 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W cyclShift ( # ` W ) ) = W )
8 1 7 sylan9eq 
 |-  ( ( N = ( # ` W ) /\ ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> ( W cyclShift N ) = W )
9 simprl 
 |-  ( ( N = ( # ` W ) /\ ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> W e. ( ClWWalks ` G ) )
10 8 9 eqeltrd 
 |-  ( ( N = ( # ` W ) /\ ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )
11 simprl 
 |-  ( ( -. N = ( # ` W ) /\ ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> W e. ( ClWWalks ` G ) )
12 df-ne 
 |-  ( N =/= ( # ` W ) <-> -. N = ( # ` W ) )
13 fzofzim 
 |-  ( ( N =/= ( # ` W ) /\ N e. ( 0 ... ( # ` W ) ) ) -> N e. ( 0 ..^ ( # ` W ) ) )
14 13 expcom 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( N =/= ( # ` W ) -> N e. ( 0 ..^ ( # ` W ) ) ) )
15 12 14 biimtrrid 
 |-  ( N e. ( 0 ... ( # ` W ) ) -> ( -. N = ( # ` W ) -> N e. ( 0 ..^ ( # ` W ) ) ) )
16 15 adantl 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( -. N = ( # ` W ) -> N e. ( 0 ..^ ( # ` W ) ) ) )
17 16 impcom 
 |-  ( ( -. N = ( # ` W ) /\ ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> N e. ( 0 ..^ ( # ` W ) ) )
18 clwwisshclwws 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )
19 11 17 18 syl2anc 
 |-  ( ( -. N = ( # ` W ) /\ ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )
20 10 19 pm2.61ian 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )