crctcshlem4

	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	crctcshlem4	$⊢ (φ \land S = 0) \to (H = F \land Q = P)$

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		oveq2	$⊢ S = 0 \to F cyclShift S = F cyclShift 0$
9		crctiswlk	$⊢ F Circuits (G) P \to F Walks (G) P$
10	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
11		cshw0	$⊢ F \in Word dom I \to F cyclShift 0 = F$
12	3 9 10 11	4syl	$⊢ φ \to F cyclShift 0 = F$
13	8 12	sylan9eqr	$⊢ (φ \land S = 0) \to F cyclShift S = F$
14	6 13	eqtrid	$⊢ (φ \land S = 0) \to H = F$
15		oveq2	$⊢ S = 0 \to N - S = N - 0$
16	1 2 3 4	crctcshlem1	$⊢ φ \to N \in ℕ_{0}$
17	16	nn0cnd	$⊢ φ \to N \in ℂ$
18	17	subid1d	$⊢ φ \to N - 0 = N$
19	15 18	sylan9eqr	$⊢ (φ \land S = 0) \to N - S = N$
20	19	breq2d	$⊢ (φ \land S = 0) \to (x \leq N - S \leftrightarrow x \leq N)$
21	20	adantr	$⊢ ((φ \land S = 0) \land x \in (0 \dots N)) \to (x \leq N - S \leftrightarrow x \leq N)$
22		oveq2	$⊢ S = 0 \to x + S = x + 0$
23	22	adantl	$⊢ (φ \land S = 0) \to x + S = x + 0$
24		elfzelz	$⊢ x \in (0 \dots N) \to x \in ℤ$
25	24	zcnd	$⊢ x \in (0 \dots N) \to x \in ℂ$
26	25	addridd	$⊢ x \in (0 \dots N) \to x + 0 = x$
27	23 26	sylan9eq	$⊢ ((φ \land S = 0) \land x \in (0 \dots N)) \to x + S = x$
28	27	fveq2d	$⊢ ((φ \land S = 0) \land x \in (0 \dots N)) \to P (x + S) = P (x)$
29	27	fvoveq1d	$⊢ ((φ \land S = 0) \land x \in (0 \dots N)) \to P (x + S - N) = P (x - N)$
30	21 28 29	ifbieq12d	$⊢ ((φ \land S = 0) \land x \in (0 \dots N)) \to if (x \leq N - S, P (x + S), P (x + S - N)) = if (x \leq N, P (x), P (x - N))$
31	30	mpteq2dva	$⊢ (φ \land S = 0) \to (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N))) = (x \in (0 \dots N) ⟼ if (x \leq N, P (x), P (x - N)))$
32		elfzle2	$⊢ x \in (0 \dots N) \to x \leq N$
33	32	adantl	$⊢ (φ \land x \in (0 \dots N)) \to x \leq N$
34	33	iftrued	$⊢ (φ \land x \in (0 \dots N)) \to if (x \leq N, P (x), P (x - N)) = P (x)$
35	34	mpteq2dva	$⊢ φ \to (x \in (0 \dots N) ⟼ if (x \leq N, P (x), P (x - N))) = (x \in (0 \dots N) ⟼ P (x))$
36	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
37	3 9 36	3syl	$⊢ φ \to P : (0 \dots \|F\|) ⟶ V$
38		ffn	$⊢ P : (0 \dots \|F\|) ⟶ V \to P Fn (0 \dots \|F\|)$
39	4	eqcomi	$⊢ \|F\| = N$
40	39	oveq2i	$⊢ (0 \dots \|F\|) = (0 \dots N)$
41	40	fneq2i	$⊢ P Fn (0 \dots \|F\|) \leftrightarrow P Fn (0 \dots N)$
42	38 41	sylib	$⊢ P : (0 \dots \|F\|) ⟶ V \to P Fn (0 \dots N)$
43	42	adantl	$⊢ (φ \land P : (0 \dots \|F\|) ⟶ V) \to P Fn (0 \dots N)$
44		dffn5	$⊢ P Fn (0 \dots N) \leftrightarrow P = (x \in (0 \dots N) ⟼ P (x))$
45	43 44	sylib	$⊢ (φ \land P : (0 \dots \|F\|) ⟶ V) \to P = (x \in (0 \dots N) ⟼ P (x))$
46	45	eqcomd	$⊢ (φ \land P : (0 \dots \|F\|) ⟶ V) \to (x \in (0 \dots N) ⟼ P (x)) = P$
47	37 46	mpdan	$⊢ φ \to (x \in (0 \dots N) ⟼ P (x)) = P$
48	35 47	eqtrd	$⊢ φ \to (x \in (0 \dots N) ⟼ if (x \leq N, P (x), P (x - N))) = P$
49	48	adantr	$⊢ (φ \land S = 0) \to (x \in (0 \dots N) ⟼ if (x \leq N, P (x), P (x - N))) = P$
50	31 49	eqtrd	$⊢ (φ \land S = 0) \to (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N))) = P$
51	7 50	eqtrid	$⊢ (φ \land S = 0) \to Q = P$
52	14 51	jca	$⊢ (φ \land S = 0) \to (H = F \land Q = P)$

Metamath Proof Explorer

Theorem crctcshlem4

Proof