eupth2lem3lem4

Description: Lemma for eupth2lem3 , formerly part of proof of eupth2lem3 : If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (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)\})$
	eupth2lem3lem3.e	$⊢ φ \to if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N)))$
	eupth2lem3lem4.i	$⊢ φ \to I (F (N)) \in 𝒫 V$
Assertion	eupth2lem3lem4	$⊢ (φ \land P (N) \neq P (N + 1) \land (U = P (N) \lor U = 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		eupth2lem3lem3.e	$⊢ φ \to if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N)))$
15		eupth2lem3lem4.i	$⊢ φ \to I (F (N)) \in 𝒫 V$
16		fvexd	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to F (N) \in V$
17	5	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to U \in V$
18	1 2 3 4 5 6	trlsegvdeglem1	$⊢ φ \to (P (N) \in V \land P (N + 1) \in V)$
19	18	simprd	$⊢ φ \to P (N + 1) \in V$
20	19	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to P (N + 1) \in V$
21		neeq1	$⊢ P (N) = U \to (P (N) \neq P (N + 1) \leftrightarrow U \neq P (N + 1))$
22	21	biimpcd	$⊢ P (N) \neq P (N + 1) \to (P (N) = U \to U \neq P (N + 1))$
23	22	adantl	$⊢ (φ \land P (N) \neq P (N + 1)) \to (P (N) = U \to U \neq P (N + 1))$
24	23	imp	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to U \neq P (N + 1)$
25	15	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to I (F (N)) \in 𝒫 V$
26	11	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
27	14	adantr	$⊢ (φ \land P (N) \neq P (N + 1)) \to if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N)))$
28		df-ne	$⊢ P (N) \neq P (N + 1) \leftrightarrow \neg P (N) = P (N + 1)$
29		ifpfal	$⊢ \neg P (N) = P (N + 1) \to (if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N))) \leftrightarrow \{P (N), P (N + 1)\} \subseteq I (F (N)))$
30	28 29	sylbi	$⊢ P (N) \neq P (N + 1) \to (if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N))) \leftrightarrow \{P (N), P (N + 1)\} \subseteq I (F (N)))$
31	30	adantl	$⊢ (φ \land P (N) \neq P (N + 1)) \to (if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N))) \leftrightarrow \{P (N), P (N + 1)\} \subseteq I (F (N)))$
32		preq1	$⊢ P (N) = U \to \{P (N), P (N + 1)\} = \{U, P (N + 1)\}$
33	32	sseq1d	$⊢ P (N) = U \to (\{P (N), P (N + 1)\} \subseteq I (F (N)) \leftrightarrow \{U, P (N + 1)\} \subseteq I (F (N)))$
34	33	biimpcd	$⊢ \{P (N), P (N + 1)\} \subseteq I (F (N)) \to (P (N) = U \to \{U, P (N + 1)\} \subseteq I (F (N)))$
35	31 34	syl6bi	$⊢ (φ \land P (N) \neq P (N + 1)) \to (if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N))) \to (P (N) = U \to \{U, P (N + 1)\} \subseteq I (F (N))))$
36	27 35	mpd	$⊢ (φ \land P (N) \neq P (N + 1)) \to (P (N) = U \to \{U, P (N + 1)\} \subseteq I (F (N)))$
37	36	imp	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to \{U, P (N + 1)\} \subseteq I (F (N))$
38	8	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to Vtx (Y) = V$
39	16 17 20 24 25 26 37 38	1hegrvtxdg1	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to VtxDeg (Y) (U) = 1$
40	39	oveq2d	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to VtxDeg (X) (U) + VtxDeg (Y) (U) = VtxDeg (X) (U) + 1$
41	40	breq2d	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to (2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow 2 ∥ (VtxDeg (X) (U) + 1))$
42	41	notbid	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow \neg 2 ∥ (VtxDeg (X) (U) + 1))$
43	1 2 3 4 5 6 7 8 9 10 11 12	eupth2lem3lem1	$⊢ φ \to VtxDeg (X) (U) \in ℕ_{0}$
44	43	nn0zd	$⊢ φ \to VtxDeg (X) (U) \in ℤ$
45		2nn	$⊢ 2 \in ℕ$
46	45	a1i	$⊢ φ \to 2 \in ℕ$
47		1lt2	$⊢ 1 < 2$
48	47	a1i	$⊢ φ \to 1 < 2$
49		ndvdsp1	$⊢ (VtxDeg (X) (U) \in ℤ \land 2 \in ℕ \land 1 < 2) \to (2 ∥ VtxDeg (X) (U) \to \neg 2 ∥ (VtxDeg (X) (U) + 1))$
50	44 46 48 49	syl3anc	$⊢ φ \to (2 ∥ VtxDeg (X) (U) \to \neg 2 ∥ (VtxDeg (X) (U) + 1))$
51	50	con2d	$⊢ φ \to (2 ∥ (VtxDeg (X) (U) + 1) \to \neg 2 ∥ VtxDeg (X) (U))$
52		1z	$⊢ 1 \in ℤ$
53		n2dvds1	$⊢ \neg 2 ∥ 1$
54		opoe	$⊢ ((VtxDeg (X) (U) \in ℤ \land \neg 2 ∥ VtxDeg (X) (U)) \land (1 \in ℤ \land \neg 2 ∥ 1)) \to 2 ∥ (VtxDeg (X) (U) + 1)$
55	52 53 54	mpanr12	$⊢ (VtxDeg (X) (U) \in ℤ \land \neg 2 ∥ VtxDeg (X) (U)) \to 2 ∥ (VtxDeg (X) (U) + 1)$
56	55	ex	$⊢ VtxDeg (X) (U) \in ℤ \to (\neg 2 ∥ VtxDeg (X) (U) \to 2 ∥ (VtxDeg (X) (U) + 1))$
57	44 56	syl	$⊢ φ \to (\neg 2 ∥ VtxDeg (X) (U) \to 2 ∥ (VtxDeg (X) (U) + 1))$
58	51 57	impbid	$⊢ φ \to (2 ∥ (VtxDeg (X) (U) + 1) \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
59		fveq2	$⊢ x = U \to VtxDeg (X) (x) = VtxDeg (X) (U)$
60	59	breq2d	$⊢ x = U \to (2 ∥ VtxDeg (X) (x) \leftrightarrow 2 ∥ VtxDeg (X) (U))$
61	60	notbid	$⊢ x = U \to (\neg 2 ∥ VtxDeg (X) (x) \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
62	61	elrab3	$⊢ U \in V \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
63	5 62	syl	$⊢ φ \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
64	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)\}))$
65	58 63 64	3bitr2d	$⊢ φ \to (2 ∥ (VtxDeg (X) (U) + 1) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
66	65	notbid	$⊢ φ \to (\neg 2 ∥ (VtxDeg (X) (U) + 1) \leftrightarrow \neg U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
67	66	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to (\neg 2 ∥ (VtxDeg (X) (U) + 1) \leftrightarrow \neg U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
68		fvex	$⊢ P (N) \in V$
69	68	eupth2lem2	$⊢ (P (N) \neq P (N + 1) \land P (N) = U) \to (\neg 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)\}))$
70	69	adantll	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to (\neg 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)\}))$
71	42 67 70	3bitrd	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N) = U) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}))$
72	71	expcom	$⊢ P (N) = U \to ((φ \land P (N) \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)\})))$
73	72	eqcoms	$⊢ U = P (N) \to ((φ \land P (N) \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)\})))$
74		fvexd	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to F (N) \in V$
75	18	simpld	$⊢ φ \to P (N) \in V$
76	75	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to P (N) \in V$
77	5	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to U \in V$
78		neeq2	$⊢ P (N + 1) = U \to (P (N) \neq P (N + 1) \leftrightarrow P (N) \neq U)$
79	78	biimpcd	$⊢ P (N) \neq P (N + 1) \to (P (N + 1) = U \to P (N) \neq U)$
80	79	adantl	$⊢ (φ \land P (N) \neq P (N + 1)) \to (P (N + 1) = U \to P (N) \neq U)$
81	80	imp	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to P (N) \neq U$
82	15	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to I (F (N)) \in 𝒫 V$
83	11	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
84		preq2	$⊢ P (N + 1) = U \to \{P (N), P (N + 1)\} = \{P (N), U\}$
85	84	sseq1d	$⊢ P (N + 1) = U \to (\{P (N), P (N + 1)\} \subseteq I (F (N)) \leftrightarrow \{P (N), U\} \subseteq I (F (N)))$
86	85	biimpcd	$⊢ \{P (N), P (N + 1)\} \subseteq I (F (N)) \to (P (N + 1) = U \to \{P (N), U\} \subseteq I (F (N)))$
87	31 86	syl6bi	$⊢ (φ \land P (N) \neq P (N + 1)) \to (if- (P (N) = P (N + 1), I (F (N)) = \{P (N)\}, \{P (N), P (N + 1)\} \subseteq I (F (N))) \to (P (N + 1) = U \to \{P (N), U\} \subseteq I (F (N))))$
88	27 87	mpd	$⊢ (φ \land P (N) \neq P (N + 1)) \to (P (N + 1) = U \to \{P (N), U\} \subseteq I (F (N)))$
89	88	imp	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to \{P (N), U\} \subseteq I (F (N))$
90	8	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to Vtx (Y) = V$
91	74 76 77 81 82 83 89 90	1hegrvtxdg1r	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to VtxDeg (Y) (U) = 1$
92	91	oveq2d	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to VtxDeg (X) (U) + VtxDeg (Y) (U) = VtxDeg (X) (U) + 1$
93	92	breq2d	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to (2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow 2 ∥ (VtxDeg (X) (U) + 1))$
94	93	notbid	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow \neg 2 ∥ (VtxDeg (X) (U) + 1))$
95	66	ad2antrr	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to (\neg 2 ∥ (VtxDeg (X) (U) + 1) \leftrightarrow \neg U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
96		necom	$⊢ P (N) \neq P (N + 1) \leftrightarrow P (N + 1) \neq P (N)$
97		fvex	$⊢ P (N + 1) \in V$
98	97	eupth2lem2	$⊢ (P (N + 1) \neq P (N) \land P (N + 1) = U) \to (\neg U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
99	96 98	sylanb	$⊢ (P (N) \neq P (N + 1) \land P (N + 1) = U) \to (\neg U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
100	99	con1bid	$⊢ (P (N) \neq P (N + 1) \land P (N + 1) = U) \to (\neg 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)\}))$
101	100	adantll	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to (\neg 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)\}))$
102	94 95 101	3bitrd	$⊢ ((φ \land P (N) \neq P (N + 1)) \land P (N + 1) = U) \to (\neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)) \leftrightarrow U \in if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\}))$
103	102	expcom	$⊢ P (N + 1) = U \to ((φ \land P (N) \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)\})))$
104	103	eqcoms	$⊢ U = P (N + 1) \to ((φ \land P (N) \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)\})))$
105	73 104	jaoi	$⊢ (U = P (N) \lor U = P (N + 1)) \to ((φ \land P (N) \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)\})))$
106	105	com12	$⊢ (φ \land P (N) \neq P (N + 1)) \to ((U = P (N) \lor U = 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)\})))$
107	106	3impia	$⊢ (φ \land P (N) \neq P (N + 1) \land (U = P (N) \lor U = 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 eupth2lem3lem4

Proof