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 30189

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 2738	. . . . . . 7 ⊢ (𝐽 + 1) = 𝐾
7	6	oveq2i 7360	. . . . . 6 ⊢ (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8		oveq1 7356	. . . . . . . . 9 ⊢ (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9		eucrct2eupth.j	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
10		elfzo0 13603	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11		nncn 12136	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12	11	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
13	10, 12	sylbi 217	. . . . . . . . . 10 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14		npcan1 11545	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
15	9, 13, 14	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
16	8, 15	sylan9eq 2784	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
17	16	oveq2d 7365	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18		eucrct2eupth.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 = (♯‘𝐹))
19	18	oveq2d 7365	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20		eucrct2eupth1.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)
21		crctiswlk 29741	. . . . . . . . . . . 12 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
22	2	wlkf 29560	. . . . . . . . . . . 12 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
23	21, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
24	20, 23	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
25		cshwn 14703	. . . . . . . . . 10 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
27	19, 26	eqtrd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
28	27	adantl 481	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
29	17, 28	eqtrd 2764	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
30	7, 29	eqtr3id 2778	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (♯‘𝐹) = (♯‘𝐹)
32	1, 2, 20, 31	crctcshlem1 29762	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐹) ∈ ℕ₀)
33		fz0sn0fz1 13548	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
35	34	eleq2d 2814	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36		elun 4104	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
37	35, 36	bitrdi 287	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38		elsni 4594	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ {0} → 𝑥 = 0)
39		0le0 12229	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
40	38, 39	eqbrtrdi 5131	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {0} → 𝑥 ≤ 0)
41	40	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → 𝑥 ≤ 0)
42	41	iftrued 4484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
43	18	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘(♯‘𝐹)))
44		crctprop 29737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
46	45	eqcomd 2735	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
47	20, 44, 46	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
48	43, 47	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0))
49	48	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑁) = (𝑃‘0))
50		oveq1 7356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
51	9, 13	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℂ)
52	51	addlidd 11317	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (0 + 𝑁) = 𝑁)
53	50, 52	sylan9eqr 2786	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
54	53	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑁))
55		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → (𝑃‘𝑥) = (𝑃‘0))
56	55	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘𝑥) = (𝑃‘0))
57	49, 54, 56	3eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
58	38, 57	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃‘𝑥))
59	42, 58	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
60	59	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
61		elfznn 13456	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62		nnnle0 12161	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
63	61, 62	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
64	63	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
65	64	iffalsed 4487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
66	61	nncnd 12144	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
67	66	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
68	51	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
69	67, 68	pncand 11476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
70	69	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃‘𝑥))
71	65, 70	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥))
72	71	ex 412	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘𝑥)))
73	60, 72	jaod 859	. . . . . . . . . 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 5185	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
77	76	adantl 481	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
78	5	oveq2i 7360	. . . . . . . . . 10 ⊢ (𝑁 − 𝐾) = (𝑁 − (𝐽 + 1))
79	8	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
80	15	oveq2d 7365	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁 − 𝑁))
81	51	subidd 11463	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 𝑁) = 0)
82	80, 81	eqtrd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
83	79, 82	sylan9eq 2784	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
84	78, 83	eqtrid 2776	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 𝐾) = 0)
85	84	breq2d 5104	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁 − 𝐾) ↔ 𝑥 ≤ 0))
86	5	oveq2i 7360	. . . . . . . . . 10 ⊢ (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
87	86	fveq2i 6825	. . . . . . . . 9 ⊢ (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
88	8	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
89	15	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
90	88, 89	sylan9eq 2784	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
91	90	fveq2d 6826	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
92	87, 91	eqtrid 2776	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
93	86	oveq1i 7359	. . . . . . . . . 10 ⊢ ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
94	93	fveq2i 6825	. . . . . . . . 9 ⊢ (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
95	88	oveq1d 7364	. . . . . . . . . . 11 ⊢ (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
96	89	oveq1d 7364	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
97	95, 96	sylan9eq 2784	. . . . . . . . . 10 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
98	97	fveq2d 6826	. . . . . . . . 9 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
99	94, 98	eqtrid 2776	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
100	85, 92, 99	ifbieq12d 4505	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101	100	mpteq2dv 5186	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
102	20, 21	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
103	1	wlkp 29562	. . . . . . . . 9 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
104		ffn 6652	. . . . . . . . 9 ⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹)))
105	102, 103, 104	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑃 Fn (0...(♯‘𝐹)))
106	105	adantl 481	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107		dffn5 6881	. . . . . . 7 ⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
108	106, 107	sylib 218	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃‘𝑥)))
109	77, 101, 108	3eqtr4d 2774	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
110	4, 30, 109	3brtr4d 5124	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
111	20	adantl 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112	111, 30, 109	3brtr4d 5124	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113		eucrct2eupth1.s	. . . 4 ⊢ (Vtx‘𝑆) = 𝑉
114		elfzolt3 13572	. . . . . . 7 ⊢ (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
115	9, 114	syl 17	. . . . . 6 ⊢ (𝜑 → 0 < 𝑁)
116		elfzoelz 13562	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
117	9, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ ℤ)
118	117	peano2zd 12583	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 + 1) ∈ ℤ)
119	5, 118	eqeltrid 2832	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
120		cshwlen 14705	. . . . . . . . 9 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121	120	eqcomd 2735	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
122	24, 119, 121	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
123	18, 122	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124	115, 123	breqtrd 5118	. . . . 5 ⊢ (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125	124	adantl 481	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126	123	adantl 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127	126	oveq1d 7364	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128		eucrct2eupth.e	. . . . . 6 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129	128	adantl 481	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
130	24, 18, 9	3jca 1128	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131	130	adantl 481	. . . . . . . 8 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132		cshimadifsn0 14737	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133	131, 132	syl 17	. . . . . . 7 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
134	7	imaeq1i 6008	. . . . . . 7 ⊢ ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135	133, 134	eqtrdi 2780	. . . . . 6 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136	135	reseq2d 5930	. . . . 5 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137	129, 136	eqtrd 2764	. . . 4 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138		eqid 2729	. . . 4 ⊢ ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
139		eqid 2729	. . . 4 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
140	1, 2, 110, 112, 113, 125, 127, 137, 138, 139	eucrct2eupth1 30188	. . 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 13581	. . . . . . . 8 ⊢ (0..^𝑁) ⊆ (0...𝑁)
145	18	oveq2d 7365	. . . . . . . 8 ⊢ (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146	144, 145	sseqtrid 3978	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147	146	resmptd 5991	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148		elfzoel2 13561	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149		fzoval 13563	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
150	9, 148, 149	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151	150	reseq2d 5930	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152	147, 151	eqtr3d 2766	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153	143, 152	eqtrid 2776	. . . 4 ⊢ (𝜑 → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154	153	adantl 481	. . 3 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155	140, 142, 154	3brtr4d 5124	. 2 ⊢ ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
156	20	adantl 481	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157		peano2nn0 12424	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℕ₀)
158	157	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ₀)
159	158	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ₀)
160		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161		1cnd 11110	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162		nn0cn 12394	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℂ)
163	162	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
164	12, 161, 163	subadd2d 11494	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165		eqcom 2736	. . . . . . . . . . . . . . 15 ⊢ (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166		eqcom 2736	. . . . . . . . . . . . . . 15 ⊢ (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167	164, 165, 166	3bitr4g 314	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168	167	necon3bbid 2962	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169	157	nn0red 12446	. . . . . . . . . . . . . . . 16 ⊢ (𝐽 ∈ ℕ₀ → (𝐽 + 1) ∈ ℝ)
170	169	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171		nnre 12135	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
172	171	3ad2ant2 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173		nn0z 12496	. . . . . . . . . . . . . . . . 17 ⊢ (𝐽 ∈ ℕ₀ → 𝐽 ∈ ℤ)
174		nnz 12492	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175		zltp1le 12525	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176	173, 174, 175	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177	176	biimp3a 1471	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178	170, 172, 177	leltned 11269	. . . . . . . . . . . . . 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 1128	. . . . . . . . . 10 ⊢ (((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183	182	ex 412	. . . . . . . . 9 ⊢ ((𝐽 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
184	10, 183	sylbi 217	. . . . . . . 8 ⊢ (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185		elfzo0 13603	. . . . . . . 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 2735	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐹) = 𝑁)
191	190	oveq2d 7365	. . . . . 6 ⊢ (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192	191	adantl 481	. . . . 5 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193	188, 189, 192	3eltr4d 2843	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194		eqid 2729	. . . 4 ⊢ (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195		eqid 2729	. . . 4 ⊢ (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
196	3	adantl 481	. . . 4 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
197	1, 2, 156, 31, 193, 194, 195, 196	eucrctshift 30187	. . 3 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198		simprl 770	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199		simprr 772	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200	124	ad2antlr 727	. . . . 5 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201	123	oveq1d 7364	. . . . . 6 ⊢ (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202	201	ad2antlr 727	. . . . 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 2780	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207	206	reseq2d 5930	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208	203, 207	eqtrd 2764	. . . . . 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 2729	. . . . 5 ⊢ ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
211	1, 2, 198, 199, 113, 200, 202, 209, 138, 210	eucrct2eupth1 30188	. . . 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 7364	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁 − 𝐾))
214	213	breq2d 5104	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
215	214	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁 − 𝐾)))
216	190	oveq2d 7365	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217	216	fveq2d 6826	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218	217	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219	215, 218	ifbieq2d 4503	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220	219	mpteq2dv 5186	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221	150	eqcomd 2735	. . . . . . . . 9 ⊢ (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222	221	adantl 481	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223	220, 222	reseq12d 5931	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
224	18	adantl 481	. . . . . . . . . 10 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225	224	oveq2d 7365	. . . . . . . . 9 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226	144, 225	sseqtrid 3978	. . . . . . . 8 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227	226	resmptd 5991	. . . . . . 7 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228	223, 227	eqtrd 2764	. . . . . 6 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229	143, 228	eqtr4id 2783	. . . . 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 5124	. . 3 ⊢ (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232	197, 231	mpdan 687	. 2 ⊢ ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233	155, 232	pm2.61ian 811	1 ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∖ cdif 3900 ∪ cun 3901 ifcif 4476 {csn 4577 class class class wbr 5092 ↦ cmpt 5173 dom cdm 5619 ↾ cres 5621 “ cima 5622 Fn wfn 6477 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 < clt 11149 ≤ cle 11150 − cmin 11347 ℕcn 12128 ℕ₀cn0 12384 ℤcz 12471 ...cfz 13410 ..^cfzo 13557 ♯chash 14237 Word cword 14420 prefix cpfx 14577 cyclShift ccsh 14694 Vtxcvtx 28941 iEdgciedg 28942 Walkscwlks 29542 Trailsctrls 29634 Circuitsccrcts 29729 EulerPathsceupth 30141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ifp 1063 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-er 8625 df-map 8755 df-pm 8756 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-n0 12385 df-z 12472 df-uz 12736 df-rp 12894 df-ico 13254 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-hash 14238 df-word 14421 df-concat 14478 df-substr 14548 df-pfx 14578 df-csh 14695 df-wlks 29545 df-trls 29636 df-crcts 29731 df-eupth 30142

This theorem is referenced by: (None)

W3C validator