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 30873

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 487	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5		eucrct2eupth.k	. . . . . . . 8 ⊢ 𝐾 = (𝐽 + 1)
6	5	eqcomi 2772	. . . . . . 7 ⊢ (𝐽 + 1) = 𝐾
7	6	oveq2i 7451	. . . . . 6 ⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8		oveq1 7447	. . . . . . . . 9 ⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9		eucrct2eupth.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
10		elfzo0 13859	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11		nncn 12367	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12	11	3ad2ant2 1152	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
13	10, 12	sylbi 220	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14		npcan1 11765	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
15	9, 13, 14	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
16	8, 15	sylan9eq 2818	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
17	16	oveq2d 7456	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18		eucrct2eupth.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (♯‘𝐹))
19	18	oveq2d 7456	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20		eucrct2eupth1.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
21		crctiswlk 30410	. . . . . . . . . . . 12 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
22	2	wlkf 30222	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
23	21, 22	syl 18	. . . . . . . . . . 11 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
24	20, 23	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
25		cshwn 14973	. . . . . . . . . 10 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
26	24, 25	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
27	19, 26	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
28	27	adantl 487	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
29	17, 28	eqtrd 2798	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
30	7, 29	eqtr3id 2812	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = (♯‘𝐹)
32	1, 2, 20, 31	crctcshlem1 30433	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ₀)
33		fz0sn0fz1 13803	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
34	32, 33	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
35	34	eleq2d 2850	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36		elun 4155	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
37	35, 36	bitrdi 290	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38		elsni 4601	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
39		0le0 12468	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
40	38, 39	eqbrtrdi 5147	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0)
41	40	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0)
42	41	iftrued 4493	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
43	18	fveq2d 6909	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹)))
44		crctprop 30406	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
46	45	eqcomd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
47	20, 44, 46	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
48	43, 47	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
49	48	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0))
50		oveq1 7447	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
51	9, 13	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℂ)
52	51	addlidd 11535	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
53	50, 52	sylan9eqr 2820	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
54	53	fveq2d 6909	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁))
55		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0))
56	55	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0))
57	49, 54, 56	3eqtr4d 2808	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
58	38, 57	sylan2 605	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
59	42, 58	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
60	59	ex 418	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
61		elfznn 13711	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62		nnnle0 12395	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
63	61, 62	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
64	63	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
65	64	iffalsed 4496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
66	61	nncnd 12375	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
67	66	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
68	51	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
69	67, 68	pncand 11694	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
70	69	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥))
71	65, 70	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
72	71	ex 418	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
73	60, 72	jaod 873	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
74	37, 73	sylbid 243	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
75	74	imp 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
76	75	mpteq2dva 5201	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
77	76	adantl 487	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
78	5	oveq2i 7451	. . . . . . . . . 10 ⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1))
79	8	oveq2d 7456	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
80	15	oveq2d 7456	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁))
81	51	subidd 11681	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
82	80, 81	eqtrd 2798	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
83	79, 82	sylan9eq 2818	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
84	78, 83	eqtrid 2810	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 𝐾) = 0)
85	84	breq2d 5118	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0))
86	5	oveq2i 7451	. . . . . . . . . 10 ⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
87	86	fveq2i 6908	. . . . . . . . 9 ⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
88	8	oveq2d 7456	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
89	15	oveq2d 7456	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
90	88, 89	sylan9eq 2818	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
91	90	fveq2d 6909	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
92	87, 91	eqtrid 2810	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
93	86	oveq1i 7450	. . . . . . . . . 10 ⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
94	93	fveq2i 6908	. . . . . . . . 9 ⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
95	88	oveq1d 7455	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
96	89	oveq1d 7455	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
97	95, 96	sylan9eq 2818	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
98	97	fveq2d 6909	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
99	94, 98	eqtrid 2810	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
100	85, 92, 99	ifbieq12d 4514	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101	100	mpteq2dv 5202	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
102	20, 21	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
103	1	wlkp 30224	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
104		ffn 6728	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹)))
105	102, 103, 104	3syl 19	. . . . . . . 8 ⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹)))
106	105	adantl 487	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107		dffn5 6963	. . . . . . 7 ⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
108	106, 107	sylib 221	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
109	77, 101, 108	3eqtr4d 2808	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
110	4, 30, 109	3brtr4d 5140	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
111	20	adantl 487	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112	111, 30, 109	3brtr4d 5140	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113		eucrct2eupth1.s	. . . 4 ⊢ (Vtx‘𝑆) = 𝑉
114		elfzolt3 13828	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
115	9, 114	syl 18	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
116		elfzoelz 13817	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
117	9, 116	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
118	117	peano2zd 12830	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
119	5, 118	eqeltrid 2868	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
120		cshwlen 14975	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121	120	eqcomd 2769	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
122	24, 119, 121	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
123	18, 122	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124	115, 123	breqtrd 5134	. . . . 5 ⊢ (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125	124	adantl 487	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126	123	adantl 487	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127	126	oveq1d 7455	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128		eucrct2eupth.e	. . . . . 6 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129	128	adantl 487	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
130	24, 18, 9	3jca 1146	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131	130	adantl 487	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132		cshimadifsn0 15006	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133	131, 132	syl 18	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
134	7	imaeq1i 6060	. . . . . . 7 ⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135	133, 134	eqtrdi 2814	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136	135	reseq2d 5980	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137	129, 136	eqtrd 2798	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138		eqid 2763	. . . 4 ⊢ ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
139		eqid 2763	. . . 4 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
140	1, 2, 110, 112, 113, 125, 127, 137, 138, 139	eucrct2eupth1 30872	. . 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 13837	. . . . . . . 8 ⊢ (0..^𝑁) ⊆ (0...𝑁)
145	18	oveq2d 7456	. . . . . . . 8 ⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146	144, 145	sseqtrid 3955	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147	146	resmptd 6043	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148		elfzoel2 13816	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149		fzoval 13818	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
150	9, 148, 149	3syl 19	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151	150	reseq2d 5980	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152	147, 151	eqtr3d 2800	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153	143, 152	eqtrid 2810	. . . 4 ⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154	153	adantl 487	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155	140, 142, 154	3brtr4d 5140	. 2 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
156	20	adantl 487	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157		peano2nn0 12670	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℕ₀)
158	157	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ₀)
159	158	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ₀)
160		simpl2 1211	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161		1cnd 11326	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162		nn0cn 12640	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℂ)
163	162	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
164	12, 161, 163	subadd2d 11712	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165		eqcom 2770	. . . . . . . . . . . . . . 15 ⊢ (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166		eqcom 2770	. . . . . . . . . . . . . . 15 ⊢ (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167	164, 165, 166	3bitr4g 317	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168	167	necon3bbid 2996	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169	157	nn0red 12692	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℝ)
170	169	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171		nnre 12366	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
172	171	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173		nn0z 12741	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℤ)
174		nnz 12738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175		zltp1le 12770	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176	173, 174, 175	syl2an 608	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177	176	biimp3a 1499	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178	170, 172, 177	leltned 11487	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁 ↔ 𝑁 ≠ (𝐽 + 1)))
179	178	biimprd 251	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180	168, 179	sylbid 243	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181	180	imp 412	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182	159, 160, 181	3jca 1146	. . . . . . . . . 10 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183	182	ex 418	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
184	10, 183	sylbi 220	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185		elfzo0 13859	. . . . . . . 8 ⊢ ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186	184, 185	imbitrrdi 255	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
187	9, 186	syl 18	. . . . . 6 ⊢ (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188	187	impcom 413	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
189	5	a1i 11	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
190	18	eqcomd 2769	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = 𝑁)
191	190	oveq2d 7456	. . . . . 6 ⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192	191	adantl 487	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193	188, 189, 192	3eltr4d 2879	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194		eqid 2763	. . . 4 ⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195		eqid 2763	. . . 4 ⊢ (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
196	3	adantl 487	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
197	1, 2, 156, 31, 193, 194, 195, 196	eucrctshift 30871	. . 3 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198		simprl 783	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199		simprr 785	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200	124	ad2antlr 740	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201	123	oveq1d 7455	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202	201	ad2antlr 740	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203	128	adantl 487	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204	130	adantl 487	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205	204, 132	syl 18	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206	205, 134	eqtrdi 2814	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207	206	reseq2d 5980	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208	203, 207	eqtrd 2798	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209	208	adantr 486	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210		eqid 2763	. . . . 5 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
211	1, 2, 198, 199, 113, 200, 202, 209, 138, 210	eucrct2eupth1 30872	. . . 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 7455	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾))
214	213	breq2d 5118	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
215	214	adantl 487	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
216	190	oveq2d 7456	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217	216	fveq2d 6909	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218	217	adantl 487	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219	215, 218	ifbieq2d 4512	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220	219	mpteq2dv 5202	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221	150	eqcomd 2769	. . . . . . . . 9 ⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222	221	adantl 487	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223	220, 222	reseq12d 5981	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
224	18	adantl 487	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225	224	oveq2d 7456	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226	144, 225	sseqtrid 3955	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227	226	resmptd 6043	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228	223, 227	eqtrd 2798	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229	143, 228	eqtr4id 2817	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230	229	adantr 486	. . . 4 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231	211, 212, 230	3brtr4d 5140	. . 3 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232	197, 231	mpdan 700	. 2 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233	155, 232	pm2.61ian 824	1 ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∖ cdif 4048 ∪ cun 4152 ifcif 4485 {csn 4588 class class class wbr 5106 ↦ cmpt 5189 dom cdm 5655 ↾ cres 5657 “ cima 5658 Fn wfn 6550 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 < clt 11367 ≤ cle 11368 − cmin 11565 ℕcn 12359 ℕ₀cn0 12630 ℤcz 12717 ...cfz 13663 ..^cfzo 13812 ♯chash 14498 Word cword 14682 prefix cpfx 14845 cyclShift ccsh 14964 Vtxcvtx 29601 iEdgciedg 29602 Walkscwlks 30204 Trailsctrls 30300 Circuitsccrcts 30398 EulerPathsceupth 30825

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-er 8742 df-map 8874 df-pm 8875 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-sup 9458 df-inf 9459 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-n0 12631 df-z 12718 df-uz 12990 df-rp 13145 df-ico 13506 df-fz 13664 df-fzo 13813 df-fl 13956 df-mod 14034 df-hash 14499 df-word 14683 df-concat 14740 df-substr 14814 df-pfx 14846 df-csh 14965 df-wlks 30207 df-trls 30302 df-crcts 30400 df-eupth 30826

This theorem is used by: (None)

W3C validator