Metamath Proof Explorer

Theorem crctcsh

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a circuit <. H , Q >. . (Contributed by AV, 10-Mar-2021) (Proof shortened by AV, 31-Oct-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 crctcsh 
|- ( ph -> H ( Circuits ` G ) Q )

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 1 2 3 4 5 6 7 crctcshlem4 
 |-  ( ( ph /\ S = 0 ) -> ( H = F /\ Q = P ) )
9 breq12 
 |-  ( ( H = F /\ Q = P ) -> ( H ( Circuits ` G ) Q <-> F ( Circuits ` G ) P ) )
10 3 9 syl5ibrcom 
 |-  ( ph -> ( ( H = F /\ Q = P ) -> H ( Circuits ` G ) Q ) )
11 10 adantr 
 |-  ( ( ph /\ S = 0 ) -> ( ( H = F /\ Q = P ) -> H ( Circuits ` G ) Q ) )
12 8 11 mpd 
 |-  ( ( ph /\ S = 0 ) -> H ( Circuits ` G ) Q )
13 1 2 3 4 5 6 7 crctcshtrl 
 |-  ( ph -> H ( Trails ` G ) Q )
14 13 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> H ( Trails ` G ) Q )
15 breq1 
 |-  ( x = 0 -> ( x <_ ( N - S ) <-> 0 <_ ( N - S ) ) )
16 oveq1 
 |-  ( x = 0 -> ( x + S ) = ( 0 + S ) )
17 16 fveq2d 
 |-  ( x = 0 -> ( P ` ( x + S ) ) = ( P ` ( 0 + S ) ) )
18 16 fvoveq1d 
 |-  ( x = 0 -> ( P ` ( ( x + S ) - N ) ) = ( P ` ( ( 0 + S ) - N ) ) )
19 15 17 18 ifbieq12d 
 |-  ( x = 0 -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = if ( 0 <_ ( N - S ) , ( P ` ( 0 + S ) ) , ( P ` ( ( 0 + S ) - N ) ) ) )
20 elfzo0le 
 |-  ( S e. ( 0 ..^ N ) -> S <_ N )
21 5 20 syl 
 |-  ( ph -> S <_ N )
22 1 2 3 4 crctcshlem1 
 |-  ( ph -> N e. NN0 )
23 22 nn0red 
 |-  ( ph -> N e. RR )
24 elfzoelz 
 |-  ( S e. ( 0 ..^ N ) -> S e. ZZ )
25 5 24 syl 
 |-  ( ph -> S e. ZZ )
26 25 zred 
 |-  ( ph -> S e. RR )
27 23 26 subge0d 
 |-  ( ph -> ( 0 <_ ( N - S ) <-> S <_ N ) )
28 21 27 mpbird 
 |-  ( ph -> 0 <_ ( N - S ) )
29 28 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> 0 <_ ( N - S ) )
30 29 iftrued 
 |-  ( ( ph /\ S =/= 0 ) -> if ( 0 <_ ( N - S ) , ( P ` ( 0 + S ) ) , ( P ` ( ( 0 + S ) - N ) ) ) = ( P ` ( 0 + S ) ) )
31 19 30 sylan9eqr 
 |-  ( ( ( ph /\ S =/= 0 ) /\ x = 0 ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = ( P ` ( 0 + S ) ) )
32 3 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> F ( Circuits ` G ) P )
33 1 2 32 4 crctcshlem1 
 |-  ( ( ph /\ S =/= 0 ) -> N e. NN0 )
34 0elfz 
 |-  ( N e. NN0 -> 0 e. ( 0 ... N ) )
35 33 34 syl 
 |-  ( ( ph /\ S =/= 0 ) -> 0 e. ( 0 ... N ) )
36 fvexd 
 |-  ( ( ph /\ S =/= 0 ) -> ( P ` ( 0 + S ) ) e. _V )
37 7 31 35 36 fvmptd2 
 |-  ( ( ph /\ S =/= 0 ) -> ( Q ` 0 ) = ( P ` ( 0 + S ) ) )
38 breq1 
 |-  ( x = ( # ` H ) -> ( x <_ ( N - S ) <-> ( # ` H ) <_ ( N - S ) ) )
39 oveq1 
 |-  ( x = ( # ` H ) -> ( x + S ) = ( ( # ` H ) + S ) )
40 39 fveq2d 
 |-  ( x = ( # ` H ) -> ( P ` ( x + S ) ) = ( P ` ( ( # ` H ) + S ) ) )
41 39 fvoveq1d 
 |-  ( x = ( # ` H ) -> ( P ` ( ( x + S ) - N ) ) = ( P ` ( ( ( # ` H ) + S ) - N ) ) )
42 38 40 41 ifbieq12d 
 |-  ( x = ( # ` H ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = if ( ( # ` H ) <_ ( N - S ) , ( P ` ( ( # ` H ) + S ) ) , ( P ` ( ( ( # ` H ) + S ) - N ) ) ) )
43 elfzoel2 
 |-  ( S e. ( 0 ..^ N ) -> N e. ZZ )
44 elfzonn0 
 |-  ( S e. ( 0 ..^ N ) -> S e. NN0 )
45 simpr 
 |-  ( ( N e. ZZ /\ S e. NN0 ) -> S e. NN0 )
46 45 anim1i 
 |-  ( ( ( N e. ZZ /\ S e. NN0 ) /\ S =/= 0 ) -> ( S e. NN0 /\ S =/= 0 ) )
47 elnnne0 
 |-  ( S e. NN <-> ( S e. NN0 /\ S =/= 0 ) )
48 46 47 sylibr 
 |-  ( ( ( N e. ZZ /\ S e. NN0 ) /\ S =/= 0 ) -> S e. NN )
49 48 nngt0d 
 |-  ( ( ( N e. ZZ /\ S e. NN0 ) /\ S =/= 0 ) -> 0 < S )
50 zre 
 |-  ( N e. ZZ -> N e. RR )
51 nn0re 
 |-  ( S e. NN0 -> S e. RR )
52 50 51 anim12ci 
 |-  ( ( N e. ZZ /\ S e. NN0 ) -> ( S e. RR /\ N e. RR ) )
53 52 adantr 
 |-  ( ( ( N e. ZZ /\ S e. NN0 ) /\ S =/= 0 ) -> ( S e. RR /\ N e. RR ) )
54 ltsubpos 
 |-  ( ( S e. RR /\ N e. RR ) -> ( 0 < S <-> ( N - S ) < N ) )
55 54 bicomd 
 |-  ( ( S e. RR /\ N e. RR ) -> ( ( N - S ) < N <-> 0 < S ) )
56 53 55 syl 
 |-  ( ( ( N e. ZZ /\ S e. NN0 ) /\ S =/= 0 ) -> ( ( N - S ) < N <-> 0 < S ) )
57 49 56 mpbird 
 |-  ( ( ( N e. ZZ /\ S e. NN0 ) /\ S =/= 0 ) -> ( N - S ) < N )
58 57 ex 
 |-  ( ( N e. ZZ /\ S e. NN0 ) -> ( S =/= 0 -> ( N - S ) < N ) )
59 43 44 58 syl2anc 
 |-  ( S e. ( 0 ..^ N ) -> ( S =/= 0 -> ( N - S ) < N ) )
60 5 59 syl 
 |-  ( ph -> ( S =/= 0 -> ( N - S ) < N ) )
61 60 imp 
 |-  ( ( ph /\ S =/= 0 ) -> ( N - S ) < N )
62 5 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> S e. ( 0 ..^ N ) )
63 1 2 32 4 62 6 crctcshlem2 
 |-  ( ( ph /\ S =/= 0 ) -> ( # ` H ) = N )
64 63 breq1d 
 |-  ( ( ph /\ S =/= 0 ) -> ( ( # ` H ) <_ ( N - S ) <-> N <_ ( N - S ) ) )
65 64 notbid 
 |-  ( ( ph /\ S =/= 0 ) -> ( -. ( # ` H ) <_ ( N - S ) <-> -. N <_ ( N - S ) ) )
66 23 26 resubcld 
 |-  ( ph -> ( N - S ) e. RR )
67 66 23 jca 
 |-  ( ph -> ( ( N - S ) e. RR /\ N e. RR ) )
68 67 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> ( ( N - S ) e. RR /\ N e. RR ) )
69 ltnle 
 |-  ( ( ( N - S ) e. RR /\ N e. RR ) -> ( ( N - S ) < N <-> -. N <_ ( N - S ) ) )
70 68 69 syl 
 |-  ( ( ph /\ S =/= 0 ) -> ( ( N - S ) < N <-> -. N <_ ( N - S ) ) )
71 65 70 bitr4d 
 |-  ( ( ph /\ S =/= 0 ) -> ( -. ( # ` H ) <_ ( N - S ) <-> ( N - S ) < N ) )
72 61 71 mpbird 
 |-  ( ( ph /\ S =/= 0 ) -> -. ( # ` H ) <_ ( N - S ) )
73 72 iffalsed 
 |-  ( ( ph /\ S =/= 0 ) -> if ( ( # ` H ) <_ ( N - S ) , ( P ` ( ( # ` H ) + S ) ) , ( P ` ( ( ( # ` H ) + S ) - N ) ) ) = ( P ` ( ( ( # ` H ) + S ) - N ) ) )
74 42 73 sylan9eqr 
 |-  ( ( ( ph /\ S =/= 0 ) /\ x = ( # ` H ) ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = ( P ` ( ( ( # ` H ) + S ) - N ) ) )
75 1 2 3 4 5 6 crctcshlem2 
 |-  ( ph -> ( # ` H ) = N )
76 75 22 eqeltrd 
 |-  ( ph -> ( # ` H ) e. NN0 )
77 76 nn0cnd 
 |-  ( ph -> ( # ` H ) e. CC )
78 25 zcnd 
 |-  ( ph -> S e. CC )
79 22 nn0cnd 
 |-  ( ph -> N e. CC )
80 77 78 79 addsubd 
 |-  ( ph -> ( ( ( # ` H ) + S ) - N ) = ( ( ( # ` H ) - N ) + S ) )
81 75 oveq1d 
 |-  ( ph -> ( ( # ` H ) - N ) = ( N - N ) )
82 79 subidd 
 |-  ( ph -> ( N - N ) = 0 )
83 81 82 eqtrd 
 |-  ( ph -> ( ( # ` H ) - N ) = 0 )
84 83 oveq1d 
 |-  ( ph -> ( ( ( # ` H ) - N ) + S ) = ( 0 + S ) )
85 80 84 eqtrd 
 |-  ( ph -> ( ( ( # ` H ) + S ) - N ) = ( 0 + S ) )
86 85 fveq2d 
 |-  ( ph -> ( P ` ( ( ( # ` H ) + S ) - N ) ) = ( P ` ( 0 + S ) ) )
87 86 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> ( P ` ( ( ( # ` H ) + S ) - N ) ) = ( P ` ( 0 + S ) ) )
88 87 adantr 
 |-  ( ( ( ph /\ S =/= 0 ) /\ x = ( # ` H ) ) -> ( P ` ( ( ( # ` H ) + S ) - N ) ) = ( P ` ( 0 + S ) ) )
89 74 88 eqtrd 
 |-  ( ( ( ph /\ S =/= 0 ) /\ x = ( # ` H ) ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = ( P ` ( 0 + S ) ) )
90 75 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> ( # ` H ) = N )
91 nn0fz0 
 |-  ( N e. NN0 <-> N e. ( 0 ... N ) )
92 22 91 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
93 92 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> N e. ( 0 ... N ) )
94 90 93 eqeltrd 
 |-  ( ( ph /\ S =/= 0 ) -> ( # ` H ) e. ( 0 ... N ) )
95 7 89 94 36 fvmptd2 
 |-  ( ( ph /\ S =/= 0 ) -> ( Q ` ( # ` H ) ) = ( P ` ( 0 + S ) ) )
96 37 95 eqtr4d 
 |-  ( ( ph /\ S =/= 0 ) -> ( Q ` 0 ) = ( Q ` ( # ` H ) ) )
97 iscrct 
 |-  ( H ( Circuits ` G ) Q <-> ( H ( Trails ` G ) Q /\ ( Q ` 0 ) = ( Q ` ( # ` H ) ) ) )
98 14 96 97 sylanbrc 
 |-  ( ( ph /\ S =/= 0 ) -> H ( Circuits ` G ) Q )
99 12 98 pm2.61dane 
 |-  ( ph -> H ( Circuits ` G ) Q )