Metamath Proof Explorer

Theorem eleclclwwlknlem1

Description: Lemma 1 for eleclclwwlkn . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypothesis erclwwlkn1.w 
|- W = ( N ClWWalksN G )
Assertion eleclclwwlknlem1 
|- ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) -> ( ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )

Proof

Step Hyp Ref Expression
1 erclwwlkn1.w 
 |-  W = ( N ClWWalksN G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 clwwlknbp 
 |-  ( Y e. ( N ClWWalksN G ) -> ( Y e. Word ( Vtx ` G ) /\ ( # ` Y ) = N ) )
4 3 1 eleq2s 
 |-  ( Y e. W -> ( Y e. Word ( Vtx ` G ) /\ ( # ` Y ) = N ) )
5 4 adantl 
 |-  ( ( X e. W /\ Y e. W ) -> ( Y e. Word ( Vtx ` G ) /\ ( # ` Y ) = N ) )
6 5 adantl 
 |-  ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) -> ( Y e. Word ( Vtx ` G ) /\ ( # ` Y ) = N ) )
7 6 adantr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) /\ ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) ) -> ( Y e. Word ( Vtx ` G ) /\ ( # ` Y ) = N ) )
8 simpl 
 |-  ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) -> K e. ( 0 ... N ) )
9 8 adantr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) /\ ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) ) -> K e. ( 0 ... N ) )
10 simpl 
 |-  ( ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> X = ( Y cyclShift K ) )
11 10 adantl 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) /\ ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) ) -> X = ( Y cyclShift K ) )
12 simprr 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) /\ ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) ) -> E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) )
13 9 11 12 3jca 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) /\ ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) ) -> ( K e. ( 0 ... N ) /\ X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) )
14 2cshwcshw 
 |-  ( ( Y e. Word ( Vtx ` G ) /\ ( # ` Y ) = N ) -> ( ( K e. ( 0 ... N ) /\ X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
15 7 13 14 sylc 
 |-  ( ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) /\ ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) )
16 15 ex 
 |-  ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) -> ( ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )