eucrct2eupth - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eucrct2eupth		Structured version Visualization version GIF version

Theorem eucrct2eupth 30337

Description: Removing one edge (𝐼‘(𝐹‘𝐽)) from a graph 𝐺 with an Eulerian circuit ⟨𝐹, 𝑃⟩ results in a graph 𝑆 with an Eulerian path ⟨𝐻, 𝑄⟩. (Contributed by AV, 17-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)

**Hypotheses**
Ref	Expression
eucrct2eupth1.v	⊢ 𝑉 = (Vtx‘𝐺)
eucrct2eupth1.i	⊢ 𝐼 = (iEdg‘𝐺)
eucrct2eupth1.d	⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)
eucrct2eupth1.c	⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
eucrct2eupth1.s	⊢ (Vtx‘𝑆) = 𝑉
eucrct2eupth.n	⊢ (𝜑 → 𝑁 = (♯‘𝐹))
eucrct2eupth.j	⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
eucrct2eupth.e	⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
eucrct2eupth.k	⊢ 𝐾 = (𝐽 + 1)
eucrct2eupth.h	⊢ 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
eucrct2eupth.q	⊢ 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))

**Assertion**
Ref	Expression
eucrct2eupth	⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)

Distinct variable groups: 𝑥,𝐹 𝑥,𝐼 𝑥,𝐽 𝑥,𝐾 𝑥,𝑁 𝑥,𝑃 𝑥,𝑉 𝜑,𝑥 Allowed substitution hints: 𝑄(𝑥) 𝑆(𝑥) 𝐺(𝑥) 𝐻(𝑥)

**Proof of Theorem eucrct2eupth**
Step	Hyp	Ref	Expression
1		eucrct2eupth1.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
2		eucrct2eupth1.i	. . . 4 ⊢ 𝐼 = (iEdg‘𝐺)
3		eucrct2eupth1.d	. . . . . 6 ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)
4	3	adantl 483	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5		eucrct2eupth.k	. . . . . . . 8 ⊢ 𝐾 = (𝐽 + 1)
6	5	eqcomi 2750	. . . . . . 7 ⊢ (𝐽 + 1) = 𝐾
7	6	oveq2i 7371	. . . . . 6 ⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8		oveq1 7367	. . . . . . . . 9 ⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9		eucrct2eupth.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
10		elfzo0 13650	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11		nncn 12177	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12	11	3ad2ant2 1141	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
13	10, 12	sylbi 219	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14		npcan1 11570	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
15	9, 13, 14	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
16	8, 15	sylan9eq 2796	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
17	16	oveq2d 7376	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18		eucrct2eupth.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (♯‘𝐹))
19	18	oveq2d 7376	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20		eucrct2eupth1.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
21		crctiswlk 29886	. . . . . . . . . . . 12 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
22	2	wlkf 29705	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
23	21, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
24	20, 23	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
25		cshwn 14754	. . . . . . . . . 10 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
27	19, 26	eqtrd 2776	. . . . . . . 8 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
28	27	adantl 483	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
29	17, 28	eqtrd 2776	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
30	7, 29	eqtr3id 2790	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31		eqid 2741	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = (♯‘𝐹)
32	1, 2, 20, 31	crctcshlem1 29907	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ₀)
33		fz0sn0fz1 13594	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
35	34	eleq2d 2827	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36		elun 4086	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
37	35, 36	bitrdi 289	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38		elsni 4575	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
39		0le0 12277	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
40	38, 39	eqbrtrdi 5114	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0)
41	40	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0)
42	41	iftrued 4465	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
43	18	fveq2d 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹)))
44		crctprop 29882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
46	45	eqcomd 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
47	20, 44, 46	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
48	43, 47	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
49	48	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0))
50		oveq1 7367	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
51	9, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℂ)
52	51	addlidd 11342	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
53	50, 52	sylan9eqr 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
54	53	fveq2d 6835	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁))
55		fveq2 6831	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0))
56	55	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0))
57	49, 54, 56	3eqtr4d 2786	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
58	38, 57	sylan2 600	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
59	42, 58	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
60	59	ex 414	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
61		elfznn 13502	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62		nnnle0 12205	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
63	61, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
64	63	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
65	64	iffalsed 4468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
66	61	nncnd 12185	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
67	66	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
68	51	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
69	67, 68	pncand 11501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
70	69	fveq2d 6835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥))
71	65, 70	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
72	71	ex 414	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
73	60, 72	jaod 866	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
74	37, 73	sylbid 242	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
75	74	imp 408	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
76	75	mpteq2dva 5168	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
77	76	adantl 483	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
78	5	oveq2i 7371	. . . . . . . . . 10 ⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1))
79	8	oveq2d 7376	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
80	15	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁))
81	51	subidd 11488	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
82	80, 81	eqtrd 2776	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
83	79, 82	sylan9eq 2796	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
84	78, 83	eqtrid 2788	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 𝐾) = 0)
85	84	breq2d 5087	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0))
86	5	oveq2i 7371	. . . . . . . . . 10 ⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
87	86	fveq2i 6834	. . . . . . . . 9 ⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
88	8	oveq2d 7376	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
89	15	oveq2d 7376	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
90	88, 89	sylan9eq 2796	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
91	90	fveq2d 6835	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
92	87, 91	eqtrid 2788	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
93	86	oveq1i 7370	. . . . . . . . . 10 ⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
94	93	fveq2i 6834	. . . . . . . . 9 ⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
95	88	oveq1d 7375	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
96	89	oveq1d 7375	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
97	95, 96	sylan9eq 2796	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
98	97	fveq2d 6835	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
99	94, 98	eqtrid 2788	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
100	85, 92, 99	ifbieq12d 4486	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101	100	mpteq2dv 5169	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
102	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
103	1	wlkp 29707	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
104		ffn 6659	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹)))
105	102, 103, 104	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹)))
106	105	adantl 483	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107		dffn5 6889	. . . . . . 7 ⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
108	106, 107	sylib 220	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
109	77, 101, 108	3eqtr4d 2786	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
110	4, 30, 109	3brtr4d 5107	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
111	20	adantl 483	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112	111, 30, 109	3brtr4d 5107	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113		eucrct2eupth1.s	. . . 4 ⊢ (Vtx‘𝑆) = 𝑉
114		elfzolt3 13619	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
115	9, 114	syl 17	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
116		elfzoelz 13608	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
117	9, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
118	117	peano2zd 12631	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
119	5, 118	eqeltrid 2845	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
120		cshwlen 14756	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121	120	eqcomd 2747	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
122	24, 119, 121	syl2anc 591	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
123	18, 122	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124	115, 123	breqtrd 5101	. . . . 5 ⊢ (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125	124	adantl 483	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126	123	adantl 483	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127	126	oveq1d 7375	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128		eucrct2eupth.e	. . . . . 6 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129	128	adantl 483	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
130	24, 18, 9	3jca 1135	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131	130	adantl 483	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132		cshimadifsn0 14787	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133	131, 132	syl 17	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
134	7	imaeq1i 6016	. . . . . . 7 ⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135	133, 134	eqtrdi 2792	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136	135	reseq2d 5938	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137	129, 136	eqtrd 2776	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138		eqid 2741	. . . 4 ⊢ ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
139		eqid 2741	. . . 4 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
140	1, 2, 110, 112, 113, 125, 127, 137, 138, 139	eucrct2eupth1 30336	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
141		eucrct2eupth.h	. . . 4 ⊢ 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
142	141	a1i 11	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)))
143		eucrct2eupth.q	. . . . 5 ⊢ 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
144		fzossfz 13628	. . . . . . . 8 ⊢ (0..^𝑁) ⊆ (0...𝑁)
145	18	oveq2d 7376	. . . . . . . 8 ⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146	144, 145	sseqtrid 3959	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147	146	resmptd 5999	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148		elfzoel2 13607	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149		fzoval 13609	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
150	9, 148, 149	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151	150	reseq2d 5938	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152	147, 151	eqtr3d 2778	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153	143, 152	eqtrid 2788	. . . 4 ⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154	153	adantl 483	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155	140, 142, 154	3brtr4d 5107	. 2 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
156	20	adantl 483	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157		peano2nn0 12472	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℕ₀)
158	157	3ad2ant1 1140	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ₀)
159	158	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ₀)
160		simpl2 1200	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161		1cnd 11134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162		nn0cn 12442	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℂ)
163	162	3ad2ant1 1140	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
164	12, 161, 163	subadd2d 11519	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165		eqcom 2748	. . . . . . . . . . . . . . 15 ⊢ (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166		eqcom 2748	. . . . . . . . . . . . . . 15 ⊢ (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167	164, 165, 166	3bitr4g 316	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168	167	necon3bbid 2973	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169	157	nn0red 12494	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℝ)
170	169	3ad2ant1 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171		nnre 12176	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
172	171	3ad2ant2 1141	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173		nn0z 12543	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℤ)
174		nnz 12540	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175		zltp1le 12572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176	173, 174, 175	syl2an 603	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177	176	biimp3a 1478	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178	170, 172, 177	leltned 11294	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁 ↔ 𝑁 ≠ (𝐽 + 1)))
179	178	biimprd 250	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180	168, 179	sylbid 242	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181	180	imp 408	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182	159, 160, 181	3jca 1135	. . . . . . . . . 10 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183	182	ex 414	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
184	10, 183	sylbi 219	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185		elfzo0 13650	. . . . . . . 8 ⊢ ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186	184, 185	imbitrrdi 254	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
187	9, 186	syl 17	. . . . . 6 ⊢ (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188	187	impcom 409	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
189	5	a1i 11	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
190	18	eqcomd 2747	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = 𝑁)
191	190	oveq2d 7376	. . . . . 6 ⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192	191	adantl 483	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193	188, 189, 192	3eltr4d 2856	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194		eqid 2741	. . . 4 ⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195		eqid 2741	. . . 4 ⊢ (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
196	3	adantl 483	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
197	1, 2, 156, 31, 193, 194, 195, 196	eucrctshift 30335	. . 3 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198		simprl 777	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199		simprr 779	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200	124	ad2antlr 734	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201	123	oveq1d 7375	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202	201	ad2antlr 734	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203	128	adantl 483	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204	130	adantl 483	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205	204, 132	syl 17	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206	205, 134	eqtrdi 2792	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207	206	reseq2d 5938	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208	203, 207	eqtrd 2776	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209	208	adantr 482	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210		eqid 2741	. . . . 5 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
211	1, 2, 198, 199, 113, 200, 202, 209, 138, 210	eucrct2eupth1 30336	. . . 4 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
212	141	a1i 11	. . . 4 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)))
213	190	oveq1d 7375	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾))
214	213	breq2d 5087	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
215	214	adantl 483	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
216	190	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217	216	fveq2d 6835	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218	217	adantl 483	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219	215, 218	ifbieq2d 4484	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220	219	mpteq2dv 5169	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221	150	eqcomd 2747	. . . . . . . . 9 ⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222	221	adantl 483	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223	220, 222	reseq12d 5939	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
224	18	adantl 483	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225	224	oveq2d 7376	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226	144, 225	sseqtrid 3959	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227	226	resmptd 5999	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228	223, 227	eqtrd 2776	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229	143, 228	eqtr4id 2795	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230	229	adantr 482	. . . 4 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231	211, 212, 230	3brtr4d 5107	. . 3 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232	197, 231	mpdan 694	. 2 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233	155, 232	pm2.61ian 818	1 ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∨ wo 854 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∖ cdif 3882 ∪ cun 3883 ifcif 4457 {csn 4558 class class class wbr 5075 ↦ cmpt 5156 dom cdm 5621 ↾ cres 5623 “ cima 5624 Fn wfn 6484 ⟶wf 6485 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 ℝcr 11032 0cc0 11033 1c1 11034 + caddc 11036 < clt 11174 ≤ cle 11175 − cmin 11372 ℕcn 12169 ℕ₀cn0 12432 ℤcz 12519 ...cfz 13456 ..^cfzo 13603 ♯chash 14287 Word cword 14470 prefix cpfx 14628 cyclShift ccsh 14745 Vtxcvtx 29087 iEdgciedg 29088 Walkscwlks 29687 Trailsctrls 29779 Circuitsccrcts 29874 EulerPathsceupth 30289

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-ifp 1070 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-map 8769 df-pm 8770 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-inf 9350 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-ico 13299 df-fz 13457 df-fzo 13604 df-fl 13746 df-mod 13824 df-hash 14288 df-word 14471 df-concat 14528 df-substr 14599 df-pfx 14629 df-csh 14746 df-wlks 29690 df-trls 29781 df-crcts 29876 df-eupth 30290

This theorem is referenced by: (None)

W3C validator