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