Metamath Proof Explorer

Theorem crctcshlem4

Description: Lemma for crctcsh . (Contributed by AV, 10-Mar-2021)

Ref Expression
Hypotheses crctcsh.v 
|- V = ( Vtx ` G )
crctcsh.i 
|- I = ( iEdg ` G )
crctcsh.d 
|- ( ph -> F ( Circuits ` G ) P )
crctcsh.n 
|- N = ( # ` F )
crctcsh.s 
|- ( ph -> S e. ( 0 ..^ N ) )
crctcsh.h 
|- H = ( F cyclShift S )
crctcsh.q 
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
Assertion crctcshlem4 
|- ( ( ph /\ S = 0 ) -> ( H = F /\ Q = P ) )

Proof

Step Hyp Ref Expression
1 crctcsh.v 
 |-  V = ( Vtx ` G )
2 crctcsh.i 
 |-  I = ( iEdg ` G )
3 crctcsh.d 
 |-  ( ph -> F ( Circuits ` G ) P )
4 crctcsh.n 
 |-  N = ( # ` F )
5 crctcsh.s 
 |-  ( ph -> S e. ( 0 ..^ N ) )
6 crctcsh.h 
 |-  H = ( F cyclShift S )
7 crctcsh.q 
 |-  Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
8 oveq2 
 |-  ( S = 0 -> ( F cyclShift S ) = ( F cyclShift 0 ) )
9 crctiswlk 
 |-  ( F ( Circuits ` G ) P -> F ( Walks ` G ) P )
10 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
11 cshw0 
 |-  ( F e. Word dom I -> ( F cyclShift 0 ) = F )
12 3 9 10 11 4syl 
 |-  ( ph -> ( F cyclShift 0 ) = F )
13 8 12 sylan9eqr 
 |-  ( ( ph /\ S = 0 ) -> ( F cyclShift S ) = F )
14 6 13 eqtrid 
 |-  ( ( ph /\ S = 0 ) -> H = F )
15 oveq2 
 |-  ( S = 0 -> ( N - S ) = ( N - 0 ) )
16 1 2 3 4 crctcshlem1 
 |-  ( ph -> N e. NN0 )
17 16 nn0cnd 
 |-  ( ph -> N e. CC )
18 17 subid1d 
 |-  ( ph -> ( N - 0 ) = N )
19 15 18 sylan9eqr 
 |-  ( ( ph /\ S = 0 ) -> ( N - S ) = N )
20 19 breq2d 
 |-  ( ( ph /\ S = 0 ) -> ( x <_ ( N - S ) <-> x <_ N ) )
21 20 adantr 
 |-  ( ( ( ph /\ S = 0 ) /\ x e. ( 0 ... N ) ) -> ( x <_ ( N - S ) <-> x <_ N ) )
22 oveq2 
 |-  ( S = 0 -> ( x + S ) = ( x + 0 ) )
23 22 adantl 
 |-  ( ( ph /\ S = 0 ) -> ( x + S ) = ( x + 0 ) )
24 elfzelz 
 |-  ( x e. ( 0 ... N ) -> x e. ZZ )
25 24 zcnd 
 |-  ( x e. ( 0 ... N ) -> x e. CC )
26 25 addridd 
 |-  ( x e. ( 0 ... N ) -> ( x + 0 ) = x )
27 23 26 sylan9eq 
 |-  ( ( ( ph /\ S = 0 ) /\ x e. ( 0 ... N ) ) -> ( x + S ) = x )
28 27 fveq2d 
 |-  ( ( ( ph /\ S = 0 ) /\ x e. ( 0 ... N ) ) -> ( P ` ( x + S ) ) = ( P ` x ) )
29 27 fvoveq1d 
 |-  ( ( ( ph /\ S = 0 ) /\ x e. ( 0 ... N ) ) -> ( P ` ( ( x + S ) - N ) ) = ( P ` ( x - N ) ) )
30 21 28 29 ifbieq12d 
 |-  ( ( ( ph /\ S = 0 ) /\ x e. ( 0 ... N ) ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = if ( x <_ N , ( P ` x ) , ( P ` ( x - N ) ) ) )
31 30 mpteq2dva 
 |-  ( ( ph /\ S = 0 ) -> ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) = ( x e. ( 0 ... N ) |-> if ( x <_ N , ( P ` x ) , ( P ` ( x - N ) ) ) ) )
32 elfzle2 
 |-  ( x e. ( 0 ... N ) -> x <_ N )
33 32 adantl 
 |-  ( ( ph /\ x e. ( 0 ... N ) ) -> x <_ N )
34 33 iftrued 
 |-  ( ( ph /\ x e. ( 0 ... N ) ) -> if ( x <_ N , ( P ` x ) , ( P ` ( x - N ) ) ) = ( P ` x ) )
35 34 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 ... N ) |-> if ( x <_ N , ( P ` x ) , ( P ` ( x - N ) ) ) ) = ( x e. ( 0 ... N ) |-> ( P ` x ) ) )
36 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
37 3 9 36 3syl 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
38 ffn 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P Fn ( 0 ... ( # ` F ) ) )
39 4 eqcomi 
 |-  ( # ` F ) = N
40 39 oveq2i 
 |-  ( 0 ... ( # ` F ) ) = ( 0 ... N )
41 40 fneq2i 
 |-  ( P Fn ( 0 ... ( # ` F ) ) <-> P Fn ( 0 ... N ) )
42 38 41 sylib 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P Fn ( 0 ... N ) )
43 42 adantl 
 |-  ( ( ph /\ P : ( 0 ... ( # ` F ) ) --> V ) -> P Fn ( 0 ... N ) )
44 dffn5 
 |-  ( P Fn ( 0 ... N ) <-> P = ( x e. ( 0 ... N ) |-> ( P ` x ) ) )
45 43 44 sylib 
 |-  ( ( ph /\ P : ( 0 ... ( # ` F ) ) --> V ) -> P = ( x e. ( 0 ... N ) |-> ( P ` x ) ) )
46 45 eqcomd 
 |-  ( ( ph /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( x e. ( 0 ... N ) |-> ( P ` x ) ) = P )
47 37 46 mpdan 
 |-  ( ph -> ( x e. ( 0 ... N ) |-> ( P ` x ) ) = P )
48 35 47 eqtrd 
 |-  ( ph -> ( x e. ( 0 ... N ) |-> if ( x <_ N , ( P ` x ) , ( P ` ( x - N ) ) ) ) = P )
49 48 adantr 
 |-  ( ( ph /\ S = 0 ) -> ( x e. ( 0 ... N ) |-> if ( x <_ N , ( P ` x ) , ( P ` ( x - N ) ) ) ) = P )
50 31 49 eqtrd 
 |-  ( ( ph /\ S = 0 ) -> ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) = P )
51 7 50 eqtrid 
 |-  ( ( ph /\ S = 0 ) -> Q = P )
52 14 51 jca 
 |-  ( ( ph /\ S = 0 ) -> ( H = F /\ Q = P ) )