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	$⊢ φ \to F Circuits (G) P$
	crctcsh.n	$⊢ N = \|F\|$
	crctcsh.s	$⊢ φ \to S \in (0 ..^N)$
	crctcsh.h	$⊢ H = F cyclShift S$
	crctcsh.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
Assertion	crctcsh	$⊢ φ \to H Circuits (G) Q$

Proof

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

Metamath Proof Explorer

Theorem crctcsh

Proof