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 ‘ 𝐺 ) 𝑄 )