eupth2lems

Description: Lemma for eupth2 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. Formerly part of proof for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

	Ref	Expression
Hypotheses	eupth2.v	$⊢ V = Vtx (G)$
	eupth2.i	$⊢ I = iEdg (G)$
	eupth2.g	$⊢ φ \to G \in UPGraph$
	eupth2.f	$⊢ φ \to Fun I$
	eupth2.p	$⊢ φ \to F EulerPaths (G) P$
Assertion	eupth2lems	$⊢ (φ \land n \in ℕ_{0}) \to ((n \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\})) \to (n + 1 \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} = if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})))$

Proof

Step	Hyp	Ref	Expression
1		eupth2.v	$⊢ V = Vtx (G)$
2		eupth2.i	$⊢ I = iEdg (G)$
3		eupth2.g	$⊢ φ \to G \in UPGraph$
4		eupth2.f	$⊢ φ \to Fun I$
5		eupth2.p	$⊢ φ \to F EulerPaths (G) P$
6		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
7	6	adantl	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℝ$
8	7	lep1d	$⊢ (φ \land n \in ℕ_{0}) \to n \leq n + 1$
9		peano2re	$⊢ n \in ℝ \to n + 1 \in ℝ$
10	7 9	syl	$⊢ (φ \land n \in ℕ_{0}) \to n + 1 \in ℝ$
11		eupthiswlk	$⊢ F EulerPaths (G) P \to F Walks (G) P$
12		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
13	5 11 12	3syl	$⊢ φ \to \|F\| \in ℕ_{0}$
14	13	nn0red	$⊢ φ \to \|F\| \in ℝ$
15	14	adantr	$⊢ (φ \land n \in ℕ_{0}) \to \|F\| \in ℝ$
16		letr	$⊢ (n \in ℝ \land n + 1 \in ℝ \land \|F\| \in ℝ) \to ((n \leq n + 1 \land n + 1 \leq \|F\|) \to n \leq \|F\|)$
17	7 10 15 16	syl3anc	$⊢ (φ \land n \in ℕ_{0}) \to ((n \leq n + 1 \land n + 1 \leq \|F\|) \to n \leq \|F\|)$
18	8 17	mpand	$⊢ (φ \land n \in ℕ_{0}) \to (n + 1 \leq \|F\| \to n \leq \|F\|)$
19	18	imim1d	$⊢ (φ \land n \in ℕ_{0}) \to ((n \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\})) \to (n + 1 \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\})))$
20		fveq2	$⊢ x = y \to VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x) = VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y)$
21	20	breq2d	$⊢ x = y \to (2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x) \leftrightarrow 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y))$
22	21	notbid	$⊢ x = y \to (\neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x) \leftrightarrow \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y))$
23	22	elrab	$⊢ y \in \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} \leftrightarrow (y \in V \land \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y))$
24	3	ad3antrrr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to G \in UPGraph$
25	4	ad3antrrr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to Fun I$
26	5	ad3antrrr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to F EulerPaths (G) P$
27		eqid	$⊢ ⟨V, {I ↾}_{F [(0 ..^n)]}⟩ = ⟨V, {I ↾}_{F [(0 ..^n)]}⟩$
28		eqid	$⊢ ⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩ = ⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩$
29		simpr	$⊢ (φ \land n \in ℕ_{0}) \to n \in ℕ_{0}$
30	29	ad2antrr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to n \in ℕ_{0}$
31		simprl	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to n + 1 \leq \|F\|$
32	31	adantr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to n + 1 \leq \|F\|$
33		simpr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to y \in V$
34		simplrr	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\})$
35	1 2 24 25 26 27 28 30 32 33 34	eupth2lem3	$⊢ (((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \land y \in V) \to (\neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y) \leftrightarrow y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}))$
36	35	pm5.32da	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to ((y \in V \land \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y)) \leftrightarrow (y \in V \land y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})))$
37		0elpw	$⊢ \emptyset \in 𝒫 V$
38	1	wlkepvtx	$⊢ F Walks (G) P \to (P (0) \in V \land P (\|F\|) \in V)$
39	38	simpld	$⊢ F Walks (G) P \to P (0) \in V$
40	5 11 39	3syl	$⊢ φ \to P (0) \in V$
41	40	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to P (0) \in V$
42	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
43	5 11 42	3syl	$⊢ φ \to P : (0 \dots \|F\|) ⟶ V$
44	43	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to P : (0 \dots \|F\|) ⟶ V$
45		peano2nn0	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ_{0}$
46	45	adantl	$⊢ (φ \land n \in ℕ_{0}) \to n + 1 \in ℕ_{0}$
47	46	adantr	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to n + 1 \in ℕ_{0}$
48		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
49	47 48	eleqtrdi	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to n + 1 \in ℤ_{\geq 0}$
50	13	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to \|F\| \in ℕ_{0}$
51	50	nn0zd	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to \|F\| \in ℤ$
52		elfz5	$⊢ (n + 1 \in ℤ_{\geq 0} \land \|F\| \in ℤ) \to (n + 1 \in (0 \dots \|F\|) \leftrightarrow n + 1 \leq \|F\|)$
53	49 51 52	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to (n + 1 \in (0 \dots \|F\|) \leftrightarrow n + 1 \leq \|F\|)$
54	31 53	mpbird	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to n + 1 \in (0 \dots \|F\|)$
55	44 54	ffvelcdmd	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to P (n + 1) \in V$
56	41 55	prssd	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to \{P (0), P (n + 1)\} \subseteq V$
57		prex	$⊢ \{P (0), P (n + 1)\} \in V$
58	57	elpw	$⊢ \{P (0), P (n + 1)\} \in 𝒫 V \leftrightarrow \{P (0), P (n + 1)\} \subseteq V$
59	56 58	sylibr	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to \{P (0), P (n + 1)\} \in 𝒫 V$
60		ifcl	$⊢ (\emptyset \in 𝒫 V \land \{P (0), P (n + 1)\} \in 𝒫 V) \to if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}) \in 𝒫 V$
61	37 59 60	sylancr	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}) \in 𝒫 V$
62	61	elpwid	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}) \subseteq V$
63	62	sseld	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to (y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}) \to y \in V)$
64	63	pm4.71rd	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to (y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}) \leftrightarrow (y \in V \land y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})))$
65	36 64	bitr4d	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to ((y \in V \land \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (y)) \leftrightarrow y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}))$
66	23 65	bitrid	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to (y \in \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} \leftrightarrow y \in if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\}))$
67	66	eqrdv	$⊢ ((φ \land n \in ℕ_{0}) \land (n + 1 \leq \|F\| \land \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}))) \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} = if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})$
68	67	exp32	$⊢ (φ \land n \in ℕ_{0}) \to (n + 1 \leq \|F\| \to (\{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\}) \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} = if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})))$
69	68	a2d	$⊢ (φ \land n \in ℕ_{0}) \to ((n + 1 \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\})) \to (n + 1 \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} = if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})))$
70	19 69	syld	$⊢ (φ \land n \in ℕ_{0}) \to ((n \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n)]}⟩) (x)\} = if (P (0) = P (n), \emptyset, \{P (0), P (n)\})) \to (n + 1 \leq \|F\| \to \{x \in V \| \neg 2 ∥ VtxDeg (⟨V, {I ↾}_{F [(0 ..^n + 1)]}⟩) (x)\} = if (P (0) = P (n + 1), \emptyset, \{P (0), P (n + 1)\})))$

Metamath Proof Explorer

Theorem eupth2lems

Proof