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 28609

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 482	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5		eucrct2eupth.k	. . . . . . . 8 ⊢ 𝐾 = (𝐽 + 1)
6	5	eqcomi 2747	. . . . . . 7 ⊢ (𝐽 + 1) = 𝐾
7	6	oveq2i 7286	. . . . . 6 ⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8		oveq1 7282	. . . . . . . . 9 ⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9		eucrct2eupth.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
10		elfzo0 13428	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11		nncn 11981	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12	11	3ad2ant2 1133	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
13	10, 12	sylbi 216	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14		npcan1 11400	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
15	9, 13, 14	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
16	8, 15	sylan9eq 2798	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
17	16	oveq2d 7291	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18		eucrct2eupth.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (♯‘𝐹))
19	18	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20		eucrct2eupth1.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
21		crctiswlk 28164	. . . . . . . . . . . 12 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
22	2	wlkf 27981	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
23	21, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
24	20, 23	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
25		cshwn 14510	. . . . . . . . . 10 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
27	19, 26	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
28	27	adantl 482	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
29	17, 28	eqtrd 2778	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
30	7, 29	eqtr3id 2792	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = (♯‘𝐹)
32	1, 2, 20, 31	crctcshlem1 28182	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ₀)
33		fz0sn0fz1 13373	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
35	34	eleq2d 2824	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36		elun 4083	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
37	35, 36	bitrdi 287	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38		elsni 4578	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
39		0le0 12074	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
40	38, 39	eqbrtrdi 5113	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0)
41	40	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0)
42	41	iftrued 4467	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
43	18	fveq2d 6778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹)))
44		crctprop 28160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
46	45	eqcomd 2744	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
47	20, 44, 46	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
48	43, 47	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
49	48	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0))
50		oveq1 7282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
51	9, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℂ)
52	51	addid2d 11176	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
53	50, 52	sylan9eqr 2800	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
54	53	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁))
55		fveq2 6774	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0))
56	55	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0))
57	49, 54, 56	3eqtr4d 2788	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
58	38, 57	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
59	42, 58	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
60	59	ex 413	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
61		elfznn 13285	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62		nnnle0 12006	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
63	61, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
64	63	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
65	64	iffalsed 4470	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
66	61	nncnd 11989	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
67	66	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
68	51	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
69	67, 68	pncand 11333	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
70	69	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥))
71	65, 70	eqtrd 2778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
72	71	ex 413	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
73	60, 72	jaod 856	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
74	37, 73	sylbid 239	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
75	74	imp 407	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
76	75	mpteq2dva 5174	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
77	76	adantl 482	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
78	5	oveq2i 7286	. . . . . . . . . 10 ⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1))
79	8	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
80	15	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁))
81	51	subidd 11320	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
82	80, 81	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
83	79, 82	sylan9eq 2798	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
84	78, 83	eqtrid 2790	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 𝐾) = 0)
85	84	breq2d 5086	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0))
86	5	oveq2i 7286	. . . . . . . . . 10 ⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
87	86	fveq2i 6777	. . . . . . . . 9 ⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
88	8	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
89	15	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
90	88, 89	sylan9eq 2798	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
91	90	fveq2d 6778	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
92	87, 91	eqtrid 2790	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
93	86	oveq1i 7285	. . . . . . . . . 10 ⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
94	93	fveq2i 6777	. . . . . . . . 9 ⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
95	88	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
96	89	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
97	95, 96	sylan9eq 2798	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
98	97	fveq2d 6778	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
99	94, 98	eqtrid 2790	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
100	85, 92, 99	ifbieq12d 4487	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101	100	mpteq2dv 5176	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
102	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
103	1	wlkp 27983	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
104		ffn 6600	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹)))
105	102, 103, 104	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹)))
106	105	adantl 482	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107		dffn5 6828	. . . . . . 7 ⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
108	106, 107	sylib 217	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
109	77, 101, 108	3eqtr4d 2788	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
110	4, 30, 109	3brtr4d 5106	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
111	20	adantl 482	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112	111, 30, 109	3brtr4d 5106	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113		eucrct2eupth1.s	. . . 4 ⊢ (Vtx‘𝑆) = 𝑉
114		elfzolt3 13397	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
115	9, 114	syl 17	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
116		elfzoelz 13387	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
117	9, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
118	117	peano2zd 12429	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
119	5, 118	eqeltrid 2843	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
120		cshwlen 14512	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121	120	eqcomd 2744	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
122	24, 119, 121	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
123	18, 122	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124	115, 123	breqtrd 5100	. . . . 5 ⊢ (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125	124	adantl 482	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126	123	adantl 482	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127	126	oveq1d 7290	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128		eucrct2eupth.e	. . . . . 6 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129	128	adantl 482	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
130	24, 18, 9	3jca 1127	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131	130	adantl 482	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132		cshimadifsn0 14543	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133	131, 132	syl 17	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
134	7	imaeq1i 5966	. . . . . . 7 ⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135	133, 134	eqtrdi 2794	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136	135	reseq2d 5891	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137	129, 136	eqtrd 2778	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138		eqid 2738	. . . 4 ⊢ ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
139		eqid 2738	. . . 4 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
140	1, 2, 110, 112, 113, 125, 127, 137, 138, 139	eucrct2eupth1 28608	. . 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 13406	. . . . . . . 8 ⊢ (0..^𝑁) ⊆ (0...𝑁)
145	18	oveq2d 7291	. . . . . . . 8 ⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146	144, 145	sseqtrid 3973	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147	146	resmptd 5948	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148		elfzoel2 13386	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149		fzoval 13388	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
150	9, 148, 149	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151	150	reseq2d 5891	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152	147, 151	eqtr3d 2780	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153	143, 152	eqtrid 2790	. . . 4 ⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154	153	adantl 482	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155	140, 142, 154	3brtr4d 5106	. 2 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
156	20	adantl 482	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157		peano2nn0 12273	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℕ₀)
158	157	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ₀)
159	158	adantr 481	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ₀)
160		simpl2 1191	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161		1cnd 10970	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162		nn0cn 12243	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℂ)
163	162	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
164	12, 161, 163	subadd2d 11351	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165		eqcom 2745	. . . . . . . . . . . . . . 15 ⊢ (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166		eqcom 2745	. . . . . . . . . . . . . . 15 ⊢ (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167	164, 165, 166	3bitr4g 314	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168	167	necon3bbid 2981	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169	157	nn0red 12294	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℝ)
170	169	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171		nnre 11980	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
172	171	3ad2ant2 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173		nn0z 12343	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℤ)
174		nnz 12342	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175		zltp1le 12370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176	173, 174, 175	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177	176	biimp3a 1468	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178	170, 172, 177	leltned 11128	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁 ↔ 𝑁 ≠ (𝐽 + 1)))
179	178	biimprd 247	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180	168, 179	sylbid 239	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181	180	imp 407	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182	159, 160, 181	3jca 1127	. . . . . . . . . 10 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183	182	ex 413	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
184	10, 183	sylbi 216	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185		elfzo0 13428	. . . . . . . 8 ⊢ ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186	184, 185	syl6ibr 251	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
187	9, 186	syl 17	. . . . . 6 ⊢ (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188	187	impcom 408	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
189	5	a1i 11	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
190	18	eqcomd 2744	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = 𝑁)
191	190	oveq2d 7291	. . . . . 6 ⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192	191	adantl 482	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193	188, 189, 192	3eltr4d 2854	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194		eqid 2738	. . . 4 ⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195		eqid 2738	. . . 4 ⊢ (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
196	3	adantl 482	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
197	1, 2, 156, 31, 193, 194, 195, 196	eucrctshift 28607	. . 3 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198		simprl 768	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199		simprr 770	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200	124	ad2antlr 724	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201	123	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202	201	ad2antlr 724	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203	128	adantl 482	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204	130	adantl 482	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205	204, 132	syl 17	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206	205, 134	eqtrdi 2794	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207	206	reseq2d 5891	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208	203, 207	eqtrd 2778	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209	208	adantr 481	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210		eqid 2738	. . . . 5 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
211	1, 2, 198, 199, 113, 200, 202, 209, 138, 210	eucrct2eupth1 28608	. . . 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 7290	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾))
214	213	breq2d 5086	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
215	214	adantl 482	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
216	190	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217	216	fveq2d 6778	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218	217	adantl 482	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219	215, 218	ifbieq2d 4485	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220	219	mpteq2dv 5176	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221	150	eqcomd 2744	. . . . . . . . 9 ⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222	221	adantl 482	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223	220, 222	reseq12d 5892	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
224	18	adantl 482	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225	224	oveq2d 7291	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226	144, 225	sseqtrid 3973	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227	226	resmptd 5948	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228	223, 227	eqtrd 2778	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229	143, 228	eqtr4id 2797	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230	229	adantr 481	. . . 4 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231	211, 212, 230	3brtr4d 5106	. . 3 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232	197, 231	mpdan 684	. 2 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233	155, 232	pm2.61ian 809	1 ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∖ cdif 3884 ∪ cun 3885 ifcif 4459 {csn 4561 class class class wbr 5074 ↦ cmpt 5157 dom cdm 5589 ↾ cres 5591 “ cima 5592 Fn wfn 6428 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 < clt 11009 ≤ cle 11010 − cmin 11205 ℕcn 11973 ℕ₀cn0 12233 ℤcz 12319 ...cfz 13239 ..^cfzo 13382 ♯chash 14044 Word cword 14217 prefix cpfx 14383 cyclShift ccsh 14501 Vtxcvtx 27366 iEdgciedg 27367 Walkscwlks 27963 Trailsctrls 28058 Circuitsccrcts 28152 EulerPathsceupth 28561

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ifp 1061 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-sup 9201 df-inf 9202 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-ico 13085 df-fz 13240 df-fzo 13383 df-fl 13512 df-mod 13590 df-hash 14045 df-word 14218 df-concat 14274 df-substr 14354 df-pfx 14384 df-csh 14502 df-wlks 27966 df-trls 28060 df-crcts 28154 df-eupth 28562

This theorem is referenced by: (None)

W3C validator