# 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}=\mathrm{Vtx}\left({G}\right)$
crctcsh.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
crctcsh.d ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
crctcsh.n ${⊢}{N}=\left|{F}\right|$
crctcsh.s ${⊢}{\phi }\to {S}\in \left(0..^{N}\right)$
crctcsh.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
crctcsh.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
Assertion crctcsh ${⊢}{\phi }\to {H}\mathrm{Circuits}\left({G}\right){Q}$

### Proof

Step Hyp Ref Expression
1 crctcsh.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 crctcsh.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 crctcsh.d ${⊢}{\phi }\to {F}\mathrm{Circuits}\left({G}\right){P}$
4 crctcsh.n ${⊢}{N}=\left|{F}\right|$
5 crctcsh.s ${⊢}{\phi }\to {S}\in \left(0..^{N}\right)$
6 crctcsh.h ${⊢}{H}={F}\mathrm{cyclShift}{S}$
7 crctcsh.q ${⊢}{Q}=\left({x}\in \left(0\dots {N}\right)⟼if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)\right)$
8 1 2 3 4 5 6 7 crctcshlem4 ${⊢}\left({\phi }\wedge {S}=0\right)\to \left({H}={F}\wedge {Q}={P}\right)$
9 breq12 ${⊢}\left({H}={F}\wedge {Q}={P}\right)\to \left({H}\mathrm{Circuits}\left({G}\right){Q}↔{F}\mathrm{Circuits}\left({G}\right){P}\right)$
10 3 9 syl5ibrcom ${⊢}{\phi }\to \left(\left({H}={F}\wedge {Q}={P}\right)\to {H}\mathrm{Circuits}\left({G}\right){Q}\right)$
11 10 adantr ${⊢}\left({\phi }\wedge {S}=0\right)\to \left(\left({H}={F}\wedge {Q}={P}\right)\to {H}\mathrm{Circuits}\left({G}\right){Q}\right)$
12 8 11 mpd ${⊢}\left({\phi }\wedge {S}=0\right)\to {H}\mathrm{Circuits}\left({G}\right){Q}$
13 1 2 3 4 5 6 7 crctcshtrl ${⊢}{\phi }\to {H}\mathrm{Trails}\left({G}\right){Q}$
14 13 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {H}\mathrm{Trails}\left({G}\right){Q}$
15 breq1 ${⊢}{x}=0\to \left({x}\le {N}-{S}↔0\le {N}-{S}\right)$
16 oveq1 ${⊢}{x}=0\to {x}+{S}=0+{S}$
17 16 fveq2d ${⊢}{x}=0\to {P}\left({x}+{S}\right)={P}\left(0+{S}\right)$
18 16 fvoveq1d ${⊢}{x}=0\to {P}\left({x}+{S}-{N}\right)={P}\left(0+{S}-{N}\right)$
19 15 17 18 ifbieq12d ${⊢}{x}=0\to if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)=if\left(0\le {N}-{S},{P}\left(0+{S}\right),{P}\left(0+{S}-{N}\right)\right)$
20 elfzo0le ${⊢}{S}\in \left(0..^{N}\right)\to {S}\le {N}$
21 5 20 syl ${⊢}{\phi }\to {S}\le {N}$
22 1 2 3 4 crctcshlem1 ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
23 22 nn0red ${⊢}{\phi }\to {N}\in ℝ$
24 elfzoelz ${⊢}{S}\in \left(0..^{N}\right)\to {S}\in ℤ$
25 5 24 syl ${⊢}{\phi }\to {S}\in ℤ$
26 25 zred ${⊢}{\phi }\to {S}\in ℝ$
27 23 26 subge0d ${⊢}{\phi }\to \left(0\le {N}-{S}↔{S}\le {N}\right)$
28 21 27 mpbird ${⊢}{\phi }\to 0\le {N}-{S}$
29 28 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to 0\le {N}-{S}$
30 29 iftrued ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to if\left(0\le {N}-{S},{P}\left(0+{S}\right),{P}\left(0+{S}-{N}\right)\right)={P}\left(0+{S}\right)$
31 19 30 sylan9eqr ${⊢}\left(\left({\phi }\wedge {S}\ne 0\right)\wedge {x}=0\right)\to if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)={P}\left(0+{S}\right)$
32 3 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {F}\mathrm{Circuits}\left({G}\right){P}$
33 1 2 32 4 crctcshlem1 ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {N}\in {ℕ}_{0}$
34 0elfz ${⊢}{N}\in {ℕ}_{0}\to 0\in \left(0\dots {N}\right)$
35 33 34 syl ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to 0\in \left(0\dots {N}\right)$
36 fvexd ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {P}\left(0+{S}\right)\in \mathrm{V}$
37 7 31 35 36 fvmptd2 ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {Q}\left(0\right)={P}\left(0+{S}\right)$
38 breq1 ${⊢}{x}=\left|{H}\right|\to \left({x}\le {N}-{S}↔\left|{H}\right|\le {N}-{S}\right)$
39 oveq1 ${⊢}{x}=\left|{H}\right|\to {x}+{S}=\left|{H}\right|+{S}$
40 39 fveq2d ${⊢}{x}=\left|{H}\right|\to {P}\left({x}+{S}\right)={P}\left(\left|{H}\right|+{S}\right)$
41 39 fvoveq1d ${⊢}{x}=\left|{H}\right|\to {P}\left({x}+{S}-{N}\right)={P}\left(\left|{H}\right|+{S}-{N}\right)$
42 38 40 41 ifbieq12d ${⊢}{x}=\left|{H}\right|\to if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)=if\left(\left|{H}\right|\le {N}-{S},{P}\left(\left|{H}\right|+{S}\right),{P}\left(\left|{H}\right|+{S}-{N}\right)\right)$
43 elfzoel2 ${⊢}{S}\in \left(0..^{N}\right)\to {N}\in ℤ$
44 elfzonn0 ${⊢}{S}\in \left(0..^{N}\right)\to {S}\in {ℕ}_{0}$
45 simpr ${⊢}\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\to {S}\in {ℕ}_{0}$
46 45 anim1i ${⊢}\left(\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\wedge {S}\ne 0\right)\to \left({S}\in {ℕ}_{0}\wedge {S}\ne 0\right)$
47 elnnne0 ${⊢}{S}\in ℕ↔\left({S}\in {ℕ}_{0}\wedge {S}\ne 0\right)$
48 46 47 sylibr ${⊢}\left(\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\wedge {S}\ne 0\right)\to {S}\in ℕ$
49 48 nngt0d ${⊢}\left(\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\wedge {S}\ne 0\right)\to 0<{S}$
50 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
51 nn0re ${⊢}{S}\in {ℕ}_{0}\to {S}\in ℝ$
52 50 51 anim12ci ${⊢}\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\to \left({S}\in ℝ\wedge {N}\in ℝ\right)$
53 52 adantr ${⊢}\left(\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\wedge {S}\ne 0\right)\to \left({S}\in ℝ\wedge {N}\in ℝ\right)$
54 ltsubpos ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left(0<{S}↔{N}-{S}<{N}\right)$
55 54 bicomd ${⊢}\left({S}\in ℝ\wedge {N}\in ℝ\right)\to \left({N}-{S}<{N}↔0<{S}\right)$
56 53 55 syl ${⊢}\left(\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\wedge {S}\ne 0\right)\to \left({N}-{S}<{N}↔0<{S}\right)$
57 49 56 mpbird ${⊢}\left(\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\wedge {S}\ne 0\right)\to {N}-{S}<{N}$
58 57 ex ${⊢}\left({N}\in ℤ\wedge {S}\in {ℕ}_{0}\right)\to \left({S}\ne 0\to {N}-{S}<{N}\right)$
59 43 44 58 syl2anc ${⊢}{S}\in \left(0..^{N}\right)\to \left({S}\ne 0\to {N}-{S}<{N}\right)$
60 5 59 syl ${⊢}{\phi }\to \left({S}\ne 0\to {N}-{S}<{N}\right)$
61 60 imp ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {N}-{S}<{N}$
62 5 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {S}\in \left(0..^{N}\right)$
63 1 2 32 4 62 6 crctcshlem2 ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left|{H}\right|={N}$
64 63 breq1d ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left(\left|{H}\right|\le {N}-{S}↔{N}\le {N}-{S}\right)$
65 64 notbid ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left(¬\left|{H}\right|\le {N}-{S}↔¬{N}\le {N}-{S}\right)$
66 23 26 resubcld ${⊢}{\phi }\to {N}-{S}\in ℝ$
67 66 23 jca ${⊢}{\phi }\to \left({N}-{S}\in ℝ\wedge {N}\in ℝ\right)$
68 67 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left({N}-{S}\in ℝ\wedge {N}\in ℝ\right)$
69 ltnle ${⊢}\left({N}-{S}\in ℝ\wedge {N}\in ℝ\right)\to \left({N}-{S}<{N}↔¬{N}\le {N}-{S}\right)$
70 68 69 syl ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left({N}-{S}<{N}↔¬{N}\le {N}-{S}\right)$
71 65 70 bitr4d ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left(¬\left|{H}\right|\le {N}-{S}↔{N}-{S}<{N}\right)$
72 61 71 mpbird ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to ¬\left|{H}\right|\le {N}-{S}$
73 72 iffalsed ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to if\left(\left|{H}\right|\le {N}-{S},{P}\left(\left|{H}\right|+{S}\right),{P}\left(\left|{H}\right|+{S}-{N}\right)\right)={P}\left(\left|{H}\right|+{S}-{N}\right)$
74 42 73 sylan9eqr ${⊢}\left(\left({\phi }\wedge {S}\ne 0\right)\wedge {x}=\left|{H}\right|\right)\to if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)={P}\left(\left|{H}\right|+{S}-{N}\right)$
75 1 2 3 4 5 6 crctcshlem2 ${⊢}{\phi }\to \left|{H}\right|={N}$
76 75 22 eqeltrd ${⊢}{\phi }\to \left|{H}\right|\in {ℕ}_{0}$
77 76 nn0cnd ${⊢}{\phi }\to \left|{H}\right|\in ℂ$
78 25 zcnd ${⊢}{\phi }\to {S}\in ℂ$
79 22 nn0cnd ${⊢}{\phi }\to {N}\in ℂ$
80 77 78 79 addsubd ${⊢}{\phi }\to \left|{H}\right|+{S}-{N}=\left|{H}\right|-{N}+{S}$
81 75 oveq1d ${⊢}{\phi }\to \left|{H}\right|-{N}={N}-{N}$
82 79 subidd ${⊢}{\phi }\to {N}-{N}=0$
83 81 82 eqtrd ${⊢}{\phi }\to \left|{H}\right|-{N}=0$
84 83 oveq1d ${⊢}{\phi }\to \left|{H}\right|-{N}+{S}=0+{S}$
85 80 84 eqtrd ${⊢}{\phi }\to \left|{H}\right|+{S}-{N}=0+{S}$
86 85 fveq2d ${⊢}{\phi }\to {P}\left(\left|{H}\right|+{S}-{N}\right)={P}\left(0+{S}\right)$
87 86 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {P}\left(\left|{H}\right|+{S}-{N}\right)={P}\left(0+{S}\right)$
88 87 adantr ${⊢}\left(\left({\phi }\wedge {S}\ne 0\right)\wedge {x}=\left|{H}\right|\right)\to {P}\left(\left|{H}\right|+{S}-{N}\right)={P}\left(0+{S}\right)$
89 74 88 eqtrd ${⊢}\left(\left({\phi }\wedge {S}\ne 0\right)\wedge {x}=\left|{H}\right|\right)\to if\left({x}\le {N}-{S},{P}\left({x}+{S}\right),{P}\left({x}+{S}-{N}\right)\right)={P}\left(0+{S}\right)$
90 75 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left|{H}\right|={N}$
91 nn0fz0 ${⊢}{N}\in {ℕ}_{0}↔{N}\in \left(0\dots {N}\right)$
92 22 91 sylib ${⊢}{\phi }\to {N}\in \left(0\dots {N}\right)$
93 92 adantr ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {N}\in \left(0\dots {N}\right)$
94 90 93 eqeltrd ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to \left|{H}\right|\in \left(0\dots {N}\right)$
95 7 89 94 36 fvmptd2 ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {Q}\left(\left|{H}\right|\right)={P}\left(0+{S}\right)$
96 37 95 eqtr4d ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {Q}\left(0\right)={Q}\left(\left|{H}\right|\right)$
97 iscrct ${⊢}{H}\mathrm{Circuits}\left({G}\right){Q}↔\left({H}\mathrm{Trails}\left({G}\right){Q}\wedge {Q}\left(0\right)={Q}\left(\left|{H}\right|\right)\right)$
98 14 96 97 sylanbrc ${⊢}\left({\phi }\wedge {S}\ne 0\right)\to {H}\mathrm{Circuits}\left({G}\right){Q}$
99 12 98 pm2.61dane ${⊢}{\phi }\to {H}\mathrm{Circuits}\left({G}\right){Q}$