eupth2lem3lem6

Description: Formerly part of proof of eupth2lem3 : If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than ( P0 ) and ( PN ) : if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 25-Feb-2021)

	Ref	Expression
Hypotheses	trlsegvdeg.v	$⊢ V = Vtx (G)$
	trlsegvdeg.i	$⊢ I = iEdg (G)$
	trlsegvdeg.f	$⊢ φ \to Fun I$
	trlsegvdeg.n	$⊢ φ \to N \in (0 ..^\|F\|)$
	trlsegvdeg.u	$⊢ φ \to U \in V$
	trlsegvdeg.w	$⊢ φ \to F Trails (G) P$
	trlsegvdeg.vx	$⊢ φ \to Vtx (X) = V$
	trlsegvdeg.vy	$⊢ φ \to Vtx (Y) = V$
	trlsegvdeg.vz	$⊢ φ \to Vtx (Z) = V$
	trlsegvdeg.ix	$⊢ φ \to iEdg (X) = {I ↾}_{F [(0 ..^N)]}$
	trlsegvdeg.iy	$⊢ φ \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
	trlsegvdeg.iz	$⊢ φ \to iEdg (Z) = {I ↾}_{F [(0 \dots N)]}$
	eupth2lem3.o	$⊢ φ \to \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} = if (P (0) = P (N), \emptyset, \{P (0), P (N)\})$
	eupth2lem3.e	$⊢ φ \to I (F (N)) = \{P (N), P (N + 1)\}$
Assertion	eupth2lem3lem6	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}))$

Proof

Step	Hyp	Ref	Expression
1		trlsegvdeg.v	$⊢ V = Vtx (G)$
2		trlsegvdeg.i	$⊢ I = iEdg (G)$
3		trlsegvdeg.f	$⊢ φ \to Fun I$
4		trlsegvdeg.n	$⊢ φ \to N \in (0 ..^\|F\|)$
5		trlsegvdeg.u	$⊢ φ \to U \in V$
6		trlsegvdeg.w	$⊢ φ \to F Trails (G) P$
7		trlsegvdeg.vx	$⊢ φ \to Vtx (X) = V$
8		trlsegvdeg.vy	$⊢ φ \to Vtx (Y) = V$
9		trlsegvdeg.vz	$⊢ φ \to Vtx (Z) = V$
10		trlsegvdeg.ix	$⊢ φ \to iEdg (X) = {I ↾}_{F [(0 ..^N)]}$
11		trlsegvdeg.iy	$⊢ φ \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
12		trlsegvdeg.iz	$⊢ φ \to iEdg (Z) = {I ↾}_{F [(0 \dots N)]}$
13		eupth2lem3.o	$⊢ φ \to \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} = if (P (0) = P (N), \emptyset, \{P (0), P (N)\})$
14		eupth2lem3.e	$⊢ φ \to I (F (N)) = \{P (N), P (N + 1)\}$
15	11	3ad2ant1	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
16	8	3ad2ant1	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to Vtx (Y) = V$
17		fvexd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to F (N) \in V$
18	5	3ad2ant1	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \in V$
19		fvexd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to I (F (N)) \in V$
20		simpl	$⊢ (U \neq P (N) \land U \neq P (N + 1)) \to U \neq P (N)$
21	20	adantl	$⊢ (P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \neq P (N)$
22		simpr	$⊢ (U \neq P (N) \land U \neq P (N + 1)) \to U \neq P (N + 1)$
23	22	adantl	$⊢ (P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \neq P (N + 1)$
24	21 23	nelprd	$⊢ (P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to \neg U \in \{P (N), P (N + 1)\}$
25		df-nel	$⊢ U \notin \{P (N), P (N + 1)\} \leftrightarrow \neg U \in \{P (N), P (N + 1)\}$
26	24 25	sylibr	$⊢ (P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \notin \{P (N), P (N + 1)\}$
27		neleq2	$⊢ I (F (N)) = \{P (N), P (N + 1)\} \to (U \notin I (F (N)) \leftrightarrow U \notin \{P (N), P (N + 1)\})$
28	26 27	imbitrrid	$⊢ I (F (N)) = \{P (N), P (N + 1)\} \to ((P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \notin I (F (N)))$
29	28	expd	$⊢ I (F (N)) = \{P (N), P (N + 1)\} \to (P (N) \neq P (N + 1) \to ((U \neq P (N) \land U \neq P (N + 1)) \to U \notin I (F (N))))$
30	14 29	syl	$⊢ φ \to (P (N) \neq P (N + 1) \to ((U \neq P (N) \land U \neq P (N + 1)) \to U \notin I (F (N))))$
31	30	3imp	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \notin I (F (N))$
32	15 16 17 18 19 31	1hevtxdg0	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to VtxDeg (Y) (U) = 0$
33	32	oveq2d	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to VtxDeg (X) (U) + VtxDeg (Y) (U) = VtxDeg (X) (U) + 0$
34	1 2 3 4 5 6 7 8 9 10 11 12	eupth2lem3lem1	$⊢ φ \to VtxDeg (X) (U) \in ℕ_{0}$
35	34	nn0cnd	$⊢ φ \to VtxDeg (X) (U) \in ℂ$
36	35	addridd	$⊢ φ \to VtxDeg (X) (U) + 0 = VtxDeg (X) (U)$
37	36	3ad2ant1	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to VtxDeg (X) (U) + 0 = VtxDeg (X) (U)$
38	33 37	eqtrd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to VtxDeg (X) (U) + VtxDeg (Y) (U) = VtxDeg (X) (U)$
39	38	breq2d	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow 2 ∥ VtxDeg (X) (U))$
40	39	notbid	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
41		fveq2	$⊢ x = U \to VtxDeg (X) (x) = VtxDeg (X) (U)$
42	41	breq2d	$⊢ x = U \to (2 ∥ VtxDeg (X) (x) \leftrightarrow 2 ∥ VtxDeg (X) (U))$
43	42	notbid	$⊢ x = U \to (\neg 2 ∥ VtxDeg (X) (x) \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
44	43	elrab3	$⊢ U \in V \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
45	5 44	syl	$⊢ φ \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
46	13	eleq2d	$⊢ φ \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
47	45 46	bitr3d	$⊢ φ \to (\neg 2 ∥ VtxDeg (X) (U) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
48	47	3ad2ant1	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (\neg 2 ∥ VtxDeg (X) (U) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
49	20	3ad2ant3	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \neq P (N)$
50	22	3ad2ant3	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to U \neq P (N + 1)$
51	49 50	2thd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U \neq P (N) \leftrightarrow U \neq P (N + 1))$
52		neeq1	$⊢ U = P (0) \to (U \neq P (N) \leftrightarrow P (0) \neq P (N))$
53		neeq1	$⊢ U = P (0) \to (U \neq P (N + 1) \leftrightarrow P (0) \neq P (N + 1))$
54	52 53	bibi12d	$⊢ U = P (0) \to ((U \neq P (N) \leftrightarrow U \neq P (N + 1)) \leftrightarrow (P (0) \neq P (N) \leftrightarrow P (0) \neq P (N + 1)))$
55	51 54	syl5ibcom	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U = P (0) \to (P (0) \neq P (N) \leftrightarrow P (0) \neq P (N + 1)))$
56	55	pm5.32rd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to ((P (0) \neq P (N) \land U = P (0)) \leftrightarrow (P (0) \neq P (N + 1) \land U = P (0)))$
57	49	neneqd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to \neg U = P (N)$
58		biorf	$⊢ \neg U = P (N) \to (U = P (0) \leftrightarrow (U = P (N) \lor U = P (0)))$
59	57 58	syl	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U = P (0) \leftrightarrow (U = P (N) \lor U = P (0)))$
60		orcom	$⊢ (U = P (N) \lor U = P (0)) \leftrightarrow (U = P (0) \lor U = P (N))$
61	59 60	bitrdi	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U = P (0) \leftrightarrow (U = P (0) \lor U = P (N)))$
62	61	anbi2d	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to ((P (0) \neq P (N) \land U = P (0)) \leftrightarrow (P (0) \neq P (N) \land (U = P (0) \lor U = P (N))))$
63	50	neneqd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to \neg U = P (N + 1)$
64		biorf	$⊢ \neg U = P (N + 1) \to (U = P (0) \leftrightarrow (U = P (N + 1) \lor U = P (0)))$
65	63 64	syl	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U = P (0) \leftrightarrow (U = P (N + 1) \lor U = P (0)))$
66		orcom	$⊢ (U = P (N + 1) \lor U = P (0)) \leftrightarrow (U = P (0) \lor U = P (N + 1))$
67	65 66	bitrdi	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U = P (0) \leftrightarrow (U = P (0) \lor U = P (N + 1)))$
68	67	anbi2d	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to ((P (0) \neq P (N + 1) \land U = P (0)) \leftrightarrow (P (0) \neq P (N + 1) \land (U = P (0) \lor U = P (N + 1))))$
69	56 62 68	3bitr3d	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to ((P (0) \neq P (N) \land (U = P (0) \lor U = P (N))) \leftrightarrow (P (0) \neq P (N + 1) \land (U = P (0) \lor U = P (N + 1))))$
70		eupth2lem1	$⊢ U \in V \to (U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}) \leftrightarrow (P (0) \neq P (N) \land (U = P (0) \lor U = P (N))))$
71	18 70	syl	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}) \leftrightarrow (P (0) \neq P (N) \land (U = P (0) \lor U = P (N))))$
72		eupth2lem1	$⊢ U \in V \to (U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}) \leftrightarrow (P (0) \neq P (N + 1) \land (U = P (0) \lor U = P (N + 1))))$
73	18 72	syl	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}) \leftrightarrow (P (0) \neq P (N + 1) \land (U = P (0) \lor U = P (N + 1))))$
74	69 71 73	3bitr4d	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}) \leftrightarrow U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}))$
75	40 48 74	3bitrd	$⊢ (φ \land P (N) \neq P (N + 1) \land (U \neq P (N) \land U \neq P (N + 1))) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}))$

Metamath Proof Explorer

Theorem eupth2lem3lem6

Proof