eucrct2eupth

Description: Removing one edge ( I( FJ ) ) from a graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . (Contributed by AV, 17-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

	Ref	Expression
Hypotheses	eucrct2eupth1.v	$⊢ V = Vtx (G)$
	eucrct2eupth1.i	$⊢ I = iEdg (G)$
	eucrct2eupth1.d	$⊢ φ \to F EulerPaths (G) P$
	eucrct2eupth1.c	$⊢ φ \to F Circuits (G) P$
	eucrct2eupth1.s	$⊢ Vtx (S) = V$
	eucrct2eupth.n	$⊢ φ \to N = \|F\|$
	eucrct2eupth.j	$⊢ φ \to J \in (0 ..^N)$
	eucrct2eupth.e	$⊢ φ \to iEdg (S) = {I ↾}_{F [(0 ..^N) ∖ \{J\}]}$
	eucrct2eupth.k	$⊢ K = J + 1$
	eucrct2eupth.h	$⊢ H = (F cyclShift K) prefix (N - 1)$
	eucrct2eupth.q	$⊢ Q = (x \in (0 ..^N) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
Assertion	eucrct2eupth	$⊢ φ \to H EulerPaths (S) Q$

Proof

Step	Hyp	Ref	Expression
1		eucrct2eupth1.v	$⊢ V = Vtx (G)$
2		eucrct2eupth1.i	$⊢ I = iEdg (G)$
3		eucrct2eupth1.d	$⊢ φ \to F EulerPaths (G) P$
4		eucrct2eupth1.c	$⊢ φ \to F Circuits (G) P$
5		eucrct2eupth1.s	$⊢ Vtx (S) = V$
6		eucrct2eupth.n	$⊢ φ \to N = \|F\|$
7		eucrct2eupth.j	$⊢ φ \to J \in (0 ..^N)$
8		eucrct2eupth.e	$⊢ φ \to iEdg (S) = {I ↾}_{F [(0 ..^N) ∖ \{J\}]}$
9		eucrct2eupth.k	$⊢ K = J + 1$
10		eucrct2eupth.h	$⊢ H = (F cyclShift K) prefix (N - 1)$
11		eucrct2eupth.q	$⊢ Q = (x \in (0 ..^N) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
12	3	adantl	$⊢ (J = N - 1 \land φ) \to F EulerPaths (G) P$
13	9	eqcomi	$⊢ J + 1 = K$
14	13	oveq2i	$⊢ F cyclShift (J + 1) = F cyclShift K$
15		oveq1	$⊢ J = N - 1 \to J + 1 = N - 1 + 1$
16		elfzo0	$⊢ J \in (0 ..^N) \leftrightarrow (J \in ℕ_{0} \land N \in ℕ \land J < N)$
17		nncn	$⊢ N \in ℕ \to N \in ℂ$
18	17	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℂ$
19	16 18	sylbi	$⊢ J \in (0 ..^N) \to N \in ℂ$
20		npcan1	$⊢ N \in ℂ \to N - 1 + 1 = N$
21	7 19 20	3syl	$⊢ φ \to N - 1 + 1 = N$
22	15 21	sylan9eq	$⊢ (J = N - 1 \land φ) \to J + 1 = N$
23	22	oveq2d	$⊢ (J = N - 1 \land φ) \to F cyclShift (J + 1) = F cyclShift N$
24	6	oveq2d	$⊢ φ \to F cyclShift N = F cyclShift \|F\|$
25		crctiswlk	$⊢ F Circuits (G) P \to F Walks (G) P$
26	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
27	25 26	syl	$⊢ F Circuits (G) P \to F \in Word dom I$
28	4 27	syl	$⊢ φ \to F \in Word dom I$
29		cshwn	$⊢ F \in Word dom I \to F cyclShift \|F\| = F$
30	28 29	syl	$⊢ φ \to F cyclShift \|F\| = F$
31	24 30	eqtrd	$⊢ φ \to F cyclShift N = F$
32	31	adantl	$⊢ (J = N - 1 \land φ) \to F cyclShift N = F$
33	23 32	eqtrd	$⊢ (J = N - 1 \land φ) \to F cyclShift (J + 1) = F$
34	14 33	syl5eqr	$⊢ (J = N - 1 \land φ) \to F cyclShift K = F$
35		eqid	$⊢ \|F\| = \|F\|$
36	1 2 4 35	crctcshlem1	$⊢ φ \to \|F\| \in ℕ_{0}$
37		fz0sn0fz1	$⊢ \|F\| \in ℕ_{0} \to (0 \dots \|F\|) = \{0\} \cup (1 \dots \|F\|)$
38	36 37	syl	$⊢ φ \to (0 \dots \|F\|) = \{0\} \cup (1 \dots \|F\|)$
39	38	eleq2d	$⊢ φ \to (x \in (0 \dots \|F\|) \leftrightarrow x \in (\{0\} \cup (1 \dots \|F\|)))$
40		elun	$⊢ x \in (\{0\} \cup (1 \dots \|F\|)) \leftrightarrow (x \in \{0\} \lor x \in (1 \dots \|F\|))$
41	39 40	syl6bb	$⊢ φ \to (x \in (0 \dots \|F\|) \leftrightarrow (x \in \{0\} \lor x \in (1 \dots \|F\|)))$
42		elsni	$⊢ x \in \{0\} \to x = 0$
43		0le0	$⊢ 0 \leq 0$
44	42 43	eqbrtrdi	$⊢ x \in \{0\} \to x \leq 0$
45	44	adantl	$⊢ (φ \land x \in \{0\}) \to x \leq 0$
46	45	iftrued	$⊢ (φ \land x \in \{0\}) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x + N)$
47	6	fveq2d	$⊢ φ \to P (N) = P (\|F\|)$
48		crctprop	$⊢ F Circuits (G) P \to (F Trails (G) P \land P (0) = P (\|F\|))$
49		simpr	$⊢ (F Trails (G) P \land P (0) = P (\|F\|)) \to P (0) = P (\|F\|)$
50	49	eqcomd	$⊢ (F Trails (G) P \land P (0) = P (\|F\|)) \to P (\|F\|) = P (0)$
51	4 48 50	3syl	$⊢ φ \to P (\|F\|) = P (0)$
52	47 51	eqtrd	$⊢ φ \to P (N) = P (0)$
53	52	adantr	$⊢ (φ \land x = 0) \to P (N) = P (0)$
54		oveq1	$⊢ x = 0 \to x + N = 0 + N$
55	7 19	syl	$⊢ φ \to N \in ℂ$
56	55	addid2d	$⊢ φ \to 0 + N = N$
57	54 56	sylan9eqr	$⊢ (φ \land x = 0) \to x + N = N$
58	57	fveq2d	$⊢ (φ \land x = 0) \to P (x + N) = P (N)$
59		fveq2	$⊢ x = 0 \to P (x) = P (0)$
60	59	adantl	$⊢ (φ \land x = 0) \to P (x) = P (0)$
61	53 58 60	3eqtr4d	$⊢ (φ \land x = 0) \to P (x + N) = P (x)$
62	42 61	sylan2	$⊢ (φ \land x \in \{0\}) \to P (x + N) = P (x)$
63	46 62	eqtrd	$⊢ (φ \land x \in \{0\}) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x)$
64	63	ex	$⊢ φ \to (x \in \{0\} \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x))$
65		elfznn	$⊢ x \in (1 \dots \|F\|) \to x \in ℕ$
66		nnnle0	$⊢ x \in ℕ \to \neg x \leq 0$
67	65 66	syl	$⊢ x \in (1 \dots \|F\|) \to \neg x \leq 0$
68	67	adantl	$⊢ (φ \land x \in (1 \dots \|F\|)) \to \neg x \leq 0$
69	68	iffalsed	$⊢ (φ \land x \in (1 \dots \|F\|)) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x + N - N)$
70	65	nncnd	$⊢ x \in (1 \dots \|F\|) \to x \in ℂ$
71	70	adantl	$⊢ (φ \land x \in (1 \dots \|F\|)) \to x \in ℂ$
72	55	adantr	$⊢ (φ \land x \in (1 \dots \|F\|)) \to N \in ℂ$
73	71 72	pncand	$⊢ (φ \land x \in (1 \dots \|F\|)) \to x + N - N = x$
74	73	fveq2d	$⊢ (φ \land x \in (1 \dots \|F\|)) \to P (x + N - N) = P (x)$
75	69 74	eqtrd	$⊢ (φ \land x \in (1 \dots \|F\|)) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x)$
76	75	ex	$⊢ φ \to (x \in (1 \dots \|F\|) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x))$
77	64 76	jaod	$⊢ φ \to ((x \in \{0\} \lor x \in (1 \dots \|F\|)) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x))$
78	41 77	sylbid	$⊢ φ \to (x \in (0 \dots \|F\|) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x))$
79	78	imp	$⊢ (φ \land x \in (0 \dots \|F\|)) \to if (x \leq 0, P (x + N), P (x + N - N)) = P (x)$
80	79	mpteq2dva	$⊢ φ \to (x \in (0 \dots \|F\|) ⟼ if (x \leq 0, P (x + N), P (x + N - N))) = (x \in (0 \dots \|F\|) ⟼ P (x))$
81	80	adantl	$⊢ (J = N - 1 \land φ) \to (x \in (0 \dots \|F\|) ⟼ if (x \leq 0, P (x + N), P (x + N - N))) = (x \in (0 \dots \|F\|) ⟼ P (x))$
82	9	oveq2i	$⊢ N - K = N - (J + 1)$
83	15	oveq2d	$⊢ J = N - 1 \to N - (J + 1) = N - (N - 1 + 1)$
84	21	oveq2d	$⊢ φ \to N - (N - 1 + 1) = N - N$
85	55	subidd	$⊢ φ \to N - N = 0$
86	84 85	eqtrd	$⊢ φ \to N - (N - 1 + 1) = 0$
87	83 86	sylan9eq	$⊢ (J = N - 1 \land φ) \to N - (J + 1) = 0$
88	82 87	syl5eq	$⊢ (J = N - 1 \land φ) \to N - K = 0$
89	88	breq2d	$⊢ (J = N - 1 \land φ) \to (x \leq N - K \leftrightarrow x \leq 0)$
90	9	oveq2i	$⊢ x + K = x + J + 1$
91	90	fveq2i	$⊢ P (x + K) = P (x + J + 1)$
92	15	oveq2d	$⊢ J = N - 1 \to x + J + 1 = x + (N - 1) + 1$
93	21	oveq2d	$⊢ φ \to x + (N - 1) + 1 = x + N$
94	92 93	sylan9eq	$⊢ (J = N - 1 \land φ) \to x + J + 1 = x + N$
95	94	fveq2d	$⊢ (J = N - 1 \land φ) \to P (x + J + 1) = P (x + N)$
96	91 95	syl5eq	$⊢ (J = N - 1 \land φ) \to P (x + K) = P (x + N)$
97	90	oveq1i	$⊢ x + K - N = x + (J + 1) - N$
98	97	fveq2i	$⊢ P (x + K - N) = P (x + (J + 1) - N)$
99	92	oveq1d	$⊢ J = N - 1 \to x + (J + 1) - N = x + (N - 1 + 1) - N$
100	93	oveq1d	$⊢ φ \to x + (N - 1 + 1) - N = x + N - N$
101	99 100	sylan9eq	$⊢ (J = N - 1 \land φ) \to x + (J + 1) - N = x + N - N$
102	101	fveq2d	$⊢ (J = N - 1 \land φ) \to P (x + (J + 1) - N) = P (x + N - N)$
103	98 102	syl5eq	$⊢ (J = N - 1 \land φ) \to P (x + K - N) = P (x + N - N)$
104	89 96 103	ifbieq12d	$⊢ (J = N - 1 \land φ) \to if (x \leq N - K, P (x + K), P (x + K - N)) = if (x \leq 0, P (x + N), P (x + N - N))$
105	104	mpteq2dv	$⊢ (J = N - 1 \land φ) \to (x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) = (x \in (0 \dots \|F\|) ⟼ if (x \leq 0, P (x + N), P (x + N - N)))$
106	4 25	syl	$⊢ φ \to F Walks (G) P$
107	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
108		ffn	$⊢ P : (0 \dots \|F\|) ⟶ V \to P Fn (0 \dots \|F\|)$
109	106 107 108	3syl	$⊢ φ \to P Fn (0 \dots \|F\|)$
110	109	adantl	$⊢ (J = N - 1 \land φ) \to P Fn (0 \dots \|F\|)$
111		dffn5	$⊢ P Fn (0 \dots \|F\|) \leftrightarrow P = (x \in (0 \dots \|F\|) ⟼ P (x))$
112	110 111	sylib	$⊢ (J = N - 1 \land φ) \to P = (x \in (0 \dots \|F\|) ⟼ P (x))$
113	81 105 112	3eqtr4d	$⊢ (J = N - 1 \land φ) \to (x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) = P$
114	12 34 113	3brtr4d	$⊢ (J = N - 1 \land φ) \to (F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
115	4	adantl	$⊢ (J = N - 1 \land φ) \to F Circuits (G) P$
116	115 34 113	3brtr4d	$⊢ (J = N - 1 \land φ) \to (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
117		elfzolt3	$⊢ J \in (0 ..^N) \to 0 < N$
118	7 117	syl	$⊢ φ \to 0 < N$
119		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
120	7 119	syl	$⊢ φ \to J \in ℤ$
121	120	peano2zd	$⊢ φ \to J + 1 \in ℤ$
122	9 121	eqeltrid	$⊢ φ \to K \in ℤ$
123		cshwlen	$⊢ (F \in Word dom I \land K \in ℤ) \to \|F cyclShift K\| = \|F\|$
124	123	eqcomd	$⊢ (F \in Word dom I \land K \in ℤ) \to \|F\| = \|F cyclShift K\|$
125	28 122 124	syl2anc	$⊢ φ \to \|F\| = \|F cyclShift K\|$
126	6 125	eqtrd	$⊢ φ \to N = \|F cyclShift K\|$
127	118 126	breqtrd	$⊢ φ \to 0 < \|F cyclShift K\|$
128	127	adantl	$⊢ (J = N - 1 \land φ) \to 0 < \|F cyclShift K\|$
129	126	adantl	$⊢ (J = N - 1 \land φ) \to N = \|F cyclShift K\|$
130	129	oveq1d	$⊢ (J = N - 1 \land φ) \to N - 1 = \|F cyclShift K\| - 1$
131	8	adantl	$⊢ (J = N - 1 \land φ) \to iEdg (S) = {I ↾}_{F [(0 ..^N) ∖ \{J\}]}$
132	28 6 7	3jca	$⊢ φ \to (F \in Word dom I \land N = \|F\| \land J \in (0 ..^N))$
133	132	adantl	$⊢ (J = N - 1 \land φ) \to (F \in Word dom I \land N = \|F\| \land J \in (0 ..^N))$
134		cshimadifsn0	$⊢ (F \in Word dom I \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift (J + 1)) [(0 ..^N - 1)]$
135	133 134	syl	$⊢ (J = N - 1 \land φ) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift (J + 1)) [(0 ..^N - 1)]$
136	14	imaeq1i	$⊢ (F cyclShift (J + 1)) [(0 ..^N - 1)] = (F cyclShift K) [(0 ..^N - 1)]$
137	135 136	syl6eq	$⊢ (J = N - 1 \land φ) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift K) [(0 ..^N - 1)]$
138	137	reseq2d	$⊢ (J = N - 1 \land φ) \to {I ↾}_{F [(0 ..^N) ∖ \{J\}]} = {I ↾}_{(F cyclShift K) [(0 ..^N - 1)]}$
139	131 138	eqtrd	$⊢ (J = N - 1 \land φ) \to iEdg (S) = {I ↾}_{(F cyclShift K) [(0 ..^N - 1)]}$
140		eqid	$⊢ (F cyclShift K) prefix (N - 1) = (F cyclShift K) prefix (N - 1)$
141		eqid	$⊢ {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)} = {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)}$
142	1 2 114 116 5 128 130 139 140 141	eucrct2eupth1	$⊢ (J = N - 1 \land φ) \to ((F cyclShift K) prefix (N - 1)) EulerPaths (S) ({(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)})$
143	10	a1i	$⊢ (J = N - 1 \land φ) \to H = (F cyclShift K) prefix (N - 1)$
144		fzossfz	$⊢ (0 ..^N) \subseteq (0 \dots N)$
145	6	oveq2d	$⊢ φ \to (0 \dots N) = (0 \dots \|F\|)$
146	144 145	sseqtrid	$⊢ φ \to (0 ..^N) \subseteq (0 \dots \|F\|)$
147	146	resmptd	$⊢ φ \to {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 ..^N)} = (x \in (0 ..^N) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
148		elfzoel2	$⊢ J \in (0 ..^N) \to N \in ℤ$
149		fzoval	$⊢ N \in ℤ \to (0 ..^N) = (0 \dots N - 1)$
150	7 148 149	3syl	$⊢ φ \to (0 ..^N) = (0 \dots N - 1)$
151	150	reseq2d	$⊢ φ \to {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 ..^N)} = {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)}$
152	147 151	eqtr3d	$⊢ φ \to (x \in (0 ..^N) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) = {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)}$
153	11 152	syl5eq	$⊢ φ \to Q = {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)}$
154	153	adantl	$⊢ (J = N - 1 \land φ) \to Q = {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 \dots N - 1)}$
155	142 143 154	3brtr4d	$⊢ (J = N - 1 \land φ) \to H EulerPaths (S) Q$
156	4	adantl	$⊢ (\neg J = N - 1 \land φ) \to F Circuits (G) P$
157		peano2nn0	$⊢ J \in ℕ_{0} \to J + 1 \in ℕ_{0}$
158	157	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J + 1 \in ℕ_{0}$
159	158	adantr	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land \neg J = N - 1) \to J + 1 \in ℕ_{0}$
160		simpl2	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land \neg J = N - 1) \to N \in ℕ$
161		1cnd	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to 1 \in ℂ$
162		nn0cn	$⊢ J \in ℕ_{0} \to J \in ℂ$
163	162	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J \in ℂ$
164	18 161 163	subadd2d	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (N - 1 = J \leftrightarrow J + 1 = N)$
165		eqcom	$⊢ J = N - 1 \leftrightarrow N - 1 = J$
166		eqcom	$⊢ N = J + 1 \leftrightarrow J + 1 = N$
167	164 165 166	3bitr4g	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J = N - 1 \leftrightarrow N = J + 1)$
168	167	necon3bbid	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (\neg J = N - 1 \leftrightarrow N \neq J + 1)$
169	157	nn0red	$⊢ J \in ℕ_{0} \to J + 1 \in ℝ$
170	169	3ad2ant1	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J + 1 \in ℝ$
171		nnre	$⊢ N \in ℕ \to N \in ℝ$
172	171	3ad2ant2	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to N \in ℝ$
173		nn0z	$⊢ J \in ℕ_{0} \to J \in ℤ$
174		nnz	$⊢ N \in ℕ \to N \in ℤ$
175		zltp1le	$⊢ (J \in ℤ \land N \in ℤ) \to (J < N \leftrightarrow J + 1 \leq N)$
176	173 174 175	syl2an	$⊢ (J \in ℕ_{0} \land N \in ℕ) \to (J < N \leftrightarrow J + 1 \leq N)$
177	176	biimp3a	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to J + 1 \leq N$
178	170 172 177	leltned	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (J + 1 < N \leftrightarrow N \neq J + 1)$
179	178	biimprd	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (N \neq J + 1 \to J + 1 < N)$
180	168 179	sylbid	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (\neg J = N - 1 \to J + 1 < N)$
181	180	imp	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land \neg J = N - 1) \to J + 1 < N$
182	159 160 181	3jca	$⊢ ((J \in ℕ_{0} \land N \in ℕ \land J < N) \land \neg J = N - 1) \to (J + 1 \in ℕ_{0} \land N \in ℕ \land J + 1 < N)$
183	182	ex	$⊢ (J \in ℕ_{0} \land N \in ℕ \land J < N) \to (\neg J = N - 1 \to (J + 1 \in ℕ_{0} \land N \in ℕ \land J + 1 < N))$
184	16 183	sylbi	$⊢ J \in (0 ..^N) \to (\neg J = N - 1 \to (J + 1 \in ℕ_{0} \land N \in ℕ \land J + 1 < N))$
185		elfzo0	$⊢ J + 1 \in (0 ..^N) \leftrightarrow (J + 1 \in ℕ_{0} \land N \in ℕ \land J + 1 < N)$
186	184 185	syl6ibr	$⊢ J \in (0 ..^N) \to (\neg J = N - 1 \to J + 1 \in (0 ..^N))$
187	7 186	syl	$⊢ φ \to (\neg J = N - 1 \to J + 1 \in (0 ..^N))$
188	187	impcom	$⊢ (\neg J = N - 1 \land φ) \to J + 1 \in (0 ..^N)$
189	9	a1i	$⊢ (\neg J = N - 1 \land φ) \to K = J + 1$
190	6	eqcomd	$⊢ φ \to \|F\| = N$
191	190	oveq2d	$⊢ φ \to (0 ..^\|F\|) = (0 ..^N)$
192	191	adantl	$⊢ (\neg J = N - 1 \land φ) \to (0 ..^\|F\|) = (0 ..^N)$
193	188 189 192	3eltr4d	$⊢ (\neg J = N - 1 \land φ) \to K \in (0 ..^\|F\|)$
194		eqid	$⊢ F cyclShift K = F cyclShift K$
195		eqid	$⊢ (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) = (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|)))$
196	3	adantl	$⊢ (\neg J = N - 1 \land φ) \to F EulerPaths (G) P$
197	1 2 156 35 193 194 195 196	eucrctshift	$⊢ (\neg J = N - 1 \land φ) \to ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))$
198		simprl	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to (F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|)))$
199		simprr	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|)))$
200	127	ad2antlr	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to 0 < \|F cyclShift K\|$
201	126	oveq1d	$⊢ φ \to N - 1 = \|F cyclShift K\| - 1$
202	201	ad2antlr	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to N - 1 = \|F cyclShift K\| - 1$
203	8	adantl	$⊢ (\neg J = N - 1 \land φ) \to iEdg (S) = {I ↾}_{F [(0 ..^N) ∖ \{J\}]}$
204	132	adantl	$⊢ (\neg J = N - 1 \land φ) \to (F \in Word dom I \land N = \|F\| \land J \in (0 ..^N))$
205	204 134	syl	$⊢ (\neg J = N - 1 \land φ) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift (J + 1)) [(0 ..^N - 1)]$
206	205 136	syl6eq	$⊢ (\neg J = N - 1 \land φ) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift K) [(0 ..^N - 1)]$
207	206	reseq2d	$⊢ (\neg J = N - 1 \land φ) \to {I ↾}_{F [(0 ..^N) ∖ \{J\}]} = {I ↾}_{(F cyclShift K) [(0 ..^N - 1)]}$
208	203 207	eqtrd	$⊢ (\neg J = N - 1 \land φ) \to iEdg (S) = {I ↾}_{(F cyclShift K) [(0 ..^N - 1)]}$
209	208	adantr	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to iEdg (S) = {I ↾}_{(F cyclShift K) [(0 ..^N - 1)]}$
210		eqid	$⊢ {(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)} = {(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)}$
211	1 2 198 199 5 200 202 209 140 210	eucrct2eupth1	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to ((F cyclShift K) prefix (N - 1)) EulerPaths (S) ({(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)})$
212	10	a1i	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to H = (F cyclShift K) prefix (N - 1)$
213	190	oveq1d	$⊢ φ \to \|F\| - K = N - K$
214	213	breq2d	$⊢ φ \to (x \leq \|F\| - K \leftrightarrow x \leq N - K)$
215	214	adantl	$⊢ (\neg J = N - 1 \land φ) \to (x \leq \|F\| - K \leftrightarrow x \leq N - K)$
216	190	oveq2d	$⊢ φ \to x + K - \|F\| = x + K - N$
217	216	fveq2d	$⊢ φ \to P (x + K - \|F\|) = P (x + K - N)$
218	217	adantl	$⊢ (\neg J = N - 1 \land φ) \to P (x + K - \|F\|) = P (x + K - N)$
219	215 218	ifbieq2d	$⊢ (\neg J = N - 1 \land φ) \to if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|)) = if (x \leq N - K, P (x + K), P (x + K - N))$
220	219	mpteq2dv	$⊢ (\neg J = N - 1 \land φ) \to (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) = (x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
221	150	eqcomd	$⊢ φ \to (0 \dots N - 1) = (0 ..^N)$
222	221	adantl	$⊢ (\neg J = N - 1 \land φ) \to (0 \dots N - 1) = (0 ..^N)$
223	220 222	reseq12d	$⊢ (\neg J = N - 1 \land φ) \to {(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)} = {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 ..^N)}$
224	6	adantl	$⊢ (\neg J = N - 1 \land φ) \to N = \|F\|$
225	224	oveq2d	$⊢ (\neg J = N - 1 \land φ) \to (0 \dots N) = (0 \dots \|F\|)$
226	144 225	sseqtrid	$⊢ (\neg J = N - 1 \land φ) \to (0 ..^N) \subseteq (0 \dots \|F\|)$
227	226	resmptd	$⊢ (\neg J = N - 1 \land φ) \to {(x \in (0 \dots \|F\|) ⟼ if (x \leq N - K, P (x + K), P (x + K - N))) ↾}_{(0 ..^N)} = (x \in (0 ..^N) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
228	223 227	eqtrd	$⊢ (\neg J = N - 1 \land φ) \to {(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)} = (x \in (0 ..^N) ⟼ if (x \leq N - K, P (x + K), P (x + K - N)))$
229	228 11	syl6reqr	$⊢ (\neg J = N - 1 \land φ) \to Q = {(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)}$
230	229	adantr	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to Q = {(x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) ↾}_{(0 \dots N - 1)}$
231	211 212 230	3brtr4d	$⊢ ((\neg J = N - 1 \land φ) \land ((F cyclShift K) EulerPaths (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))) \land (F cyclShift K) Circuits (G) (x \in (0 \dots \|F\|) ⟼ if (x \leq \|F\| - K, P (x + K), P (x + K - \|F\|))))) \to H EulerPaths (S) Q$
232	197 231	mpdan	$⊢ (\neg J = N - 1 \land φ) \to H EulerPaths (S) Q$
233	155 232	pm2.61ian	$⊢ φ \to H EulerPaths (S) Q$

Metamath Proof Explorer

Theorem eucrct2eupth

Proof