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

Metamath Proof Explorer

Theorem crctcshlem4

Proof