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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
crctcsh.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
crctcsh.d ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
crctcsh.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
crctcsh.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
crctcsh.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
crctcsh.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
Assertion crctcsh ( 𝜑 → 𝐻 ( Circuits ‘ 𝐺 ) 𝑄 )

Proof

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