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 30334

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 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5		eucrct2eupth.k	. . . . . . . 8 ⊢ 𝐾 = (𝐽 + 1)
6	5	eqcomi 2746	. . . . . . 7 ⊢ (𝐽 + 1) = 𝐾
7	6	oveq2i 7373	. . . . . 6 ⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8		oveq1 7369	. . . . . . . . 9 ⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9		eucrct2eupth.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
10		elfzo0 13650	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11		nncn 12177	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12	11	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
13	10, 12	sylbi 217	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14		npcan1 11570	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
15	9, 13, 14	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
16	8, 15	sylan9eq 2792	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
17	16	oveq2d 7378	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18		eucrct2eupth.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (♯‘𝐹))
19	18	oveq2d 7378	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20		eucrct2eupth1.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
21		crctiswlk 29883	. . . . . . . . . . . 12 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
22	2	wlkf 29702	. . . . . . . . . . . 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 2772	. . . . . . . 8 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
28	27	adantl 481	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
29	17, 28	eqtrd 2772	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
30	7, 29	eqtr3id 2786	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = (♯‘𝐹)
32	1, 2, 20, 31	crctcshlem1 29904	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ₀)
33		fz0sn0fz1 13594	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
35	34	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36		elun 4094	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
37	35, 36	bitrdi 287	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38		elsni 4585	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
39		0le0 12277	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
40	38, 39	eqbrtrdi 5125	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0)
41	40	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0)
42	41	iftrued 4475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
43	18	fveq2d 6840	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹)))
44		crctprop 29879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
46	45	eqcomd 2743	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
47	20, 44, 46	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
48	43, 47	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
49	48	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0))
50		oveq1 7369	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
51	9, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℂ)
52	51	addlidd 11342	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
53	50, 52	sylan9eqr 2794	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
54	53	fveq2d 6840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁))
55		fveq2 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0))
56	55	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0))
57	49, 54, 56	3eqtr4d 2782	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
58	38, 57	sylan2 594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
59	42, 58	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
60	59	ex 412	. . . . . . . . . . 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 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
65	64	iffalsed 4478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
66	61	nncnd 12185	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
67	66	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
68	51	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
69	67, 68	pncand 11501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
70	69	fveq2d 6840	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥))
71	65, 70	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
72	71	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
73	60, 72	jaod 860	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
74	37, 73	sylbid 240	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
75	74	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
76	75	mpteq2dva 5179	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
77	76	adantl 481	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
78	5	oveq2i 7373	. . . . . . . . . 10 ⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1))
79	8	oveq2d 7378	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
80	15	oveq2d 7378	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁))
81	51	subidd 11488	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
82	80, 81	eqtrd 2772	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
83	79, 82	sylan9eq 2792	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
84	78, 83	eqtrid 2784	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 𝐾) = 0)
85	84	breq2d 5098	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0))
86	5	oveq2i 7373	. . . . . . . . . 10 ⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
87	86	fveq2i 6839	. . . . . . . . 9 ⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
88	8	oveq2d 7378	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
89	15	oveq2d 7378	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
90	88, 89	sylan9eq 2792	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
91	90	fveq2d 6840	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
92	87, 91	eqtrid 2784	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
93	86	oveq1i 7372	. . . . . . . . . 10 ⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
94	93	fveq2i 6839	. . . . . . . . 9 ⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
95	88	oveq1d 7377	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
96	89	oveq1d 7377	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
97	95, 96	sylan9eq 2792	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
98	97	fveq2d 6840	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
99	94, 98	eqtrid 2784	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
100	85, 92, 99	ifbieq12d 4496	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101	100	mpteq2dv 5180	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
102	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
103	1	wlkp 29704	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
104		ffn 6664	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹)))
105	102, 103, 104	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹)))
106	105	adantl 481	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107		dffn5 6894	. . . . . . 7 ⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
108	106, 107	sylib 218	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
109	77, 101, 108	3eqtr4d 2782	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
110	4, 30, 109	3brtr4d 5118	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
111	20	adantl 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112	111, 30, 109	3brtr4d 5118	. . . 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 2841	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
120		cshwlen 14756	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121	120	eqcomd 2743	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
122	24, 119, 121	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
123	18, 122	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124	115, 123	breqtrd 5112	. . . . 5 ⊢ (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125	124	adantl 481	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126	123	adantl 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127	126	oveq1d 7377	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128		eucrct2eupth.e	. . . . . 6 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129	128	adantl 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
130	24, 18, 9	3jca 1129	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131	130	adantl 481	. . . . . . . 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 6018	. . . . . . 7 ⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135	133, 134	eqtrdi 2788	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136	135	reseq2d 5940	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137	129, 136	eqtrd 2772	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138		eqid 2737	. . . 4 ⊢ ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
139		eqid 2737	. . . 4 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
140	1, 2, 110, 112, 113, 125, 127, 137, 138, 139	eucrct2eupth1 30333	. . 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 7378	. . . . . . . 8 ⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146	144, 145	sseqtrid 3965	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147	146	resmptd 6001	. . . . . 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 5940	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152	147, 151	eqtr3d 2774	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153	143, 152	eqtrid 2784	. . . 4 ⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154	153	adantl 481	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155	140, 142, 154	3brtr4d 5118	. 2 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
156	20	adantl 481	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157		peano2nn0 12472	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℕ₀)
158	157	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ₀)
159	158	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ₀)
160		simpl2 1194	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161		1cnd 11134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162		nn0cn 12442	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℂ)
163	162	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
164	12, 161, 163	subadd2d 11519	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166		eqcom 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167	164, 165, 166	3bitr4g 314	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168	167	necon3bbid 2970	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169	157	nn0red 12494	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℝ)
170	169	3ad2ant1 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171		nnre 12176	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
172	171	3ad2ant2 1135	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173		nn0z 12543	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℤ)
174		nnz 12540	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175		zltp1le 12572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176	173, 174, 175	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177	176	biimp3a 1472	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178	170, 172, 177	leltned 11294	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁 ↔ 𝑁 ≠ (𝐽 + 1)))
179	178	biimprd 248	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180	168, 179	sylbid 240	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181	180	imp 406	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182	159, 160, 181	3jca 1129	. . . . . . . . . 10 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183	182	ex 412	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
184	10, 183	sylbi 217	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185		elfzo0 13650	. . . . . . . 8 ⊢ ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186	184, 185	imbitrrdi 252	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
187	9, 186	syl 17	. . . . . 6 ⊢ (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188	187	impcom 407	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
189	5	a1i 11	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
190	18	eqcomd 2743	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = 𝑁)
191	190	oveq2d 7378	. . . . . 6 ⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192	191	adantl 481	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193	188, 189, 192	3eltr4d 2852	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194		eqid 2737	. . . 4 ⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195		eqid 2737	. . . 4 ⊢ (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
196	3	adantl 481	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
197	1, 2, 156, 31, 193, 194, 195, 196	eucrctshift 30332	. . 3 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198		simprl 771	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199		simprr 773	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200	124	ad2antlr 728	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201	123	oveq1d 7377	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202	201	ad2antlr 728	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203	128	adantl 481	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204	130	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205	204, 132	syl 17	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206	205, 134	eqtrdi 2788	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207	206	reseq2d 5940	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208	203, 207	eqtrd 2772	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209	208	adantr 480	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210		eqid 2737	. . . . 5 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
211	1, 2, 198, 199, 113, 200, 202, 209, 138, 210	eucrct2eupth1 30333	. . . 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 7377	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾))
214	213	breq2d 5098	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
215	214	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
216	190	oveq2d 7378	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217	216	fveq2d 6840	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218	217	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219	215, 218	ifbieq2d 4494	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220	219	mpteq2dv 5180	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221	150	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222	221	adantl 481	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223	220, 222	reseq12d 5941	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
224	18	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225	224	oveq2d 7378	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226	144, 225	sseqtrid 3965	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227	226	resmptd 6001	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228	223, 227	eqtrd 2772	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229	143, 228	eqtr4id 2791	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230	229	adantr 480	. . . 4 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231	211, 212, 230	3brtr4d 5118	. . 3 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232	197, 231	mpdan 688	. 2 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233	155, 232	pm2.61ian 812	1 ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∖ cdif 3887 ∪ cun 3888 ifcif 4467 {csn 4568 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5626 ↾ cres 5628 “ cima 5629 Fn wfn 6489 ⟶wf 6490 ‘cfv 6494 (class class class)co 7362 ℂ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 29083 iEdgciedg 29084 Walkscwlks 29684 Trailsctrls 29776 Circuitsccrcts 29871 EulerPathsceupth 30286

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 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 207 df-an 396 df-or 849 df-ifp 1064 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-er 8638 df-map 8770 df-pm 8771 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-sup 9350 df-inf 9351 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 29687 df-trls 29778 df-crcts 29873 df-eupth 30287

This theorem is referenced by: (None)

W3C validator