eupth2lem3lem3

Description: Lemma for eupth2lem3 , formerly part of proof of eupth2lem3 : If a loop { ( PN ) , ( P( N + 1 ) ) } is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 21-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)))$
Assertion	eupth2lem3lem3	$⊢ (φ \land P (N) = 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		fveq2	$⊢ x = U \to VtxDeg (X) (x) = VtxDeg (X) (U)$
16	15	breq2d	$⊢ x = U \to (2 ∥ VtxDeg (X) (x) \leftrightarrow 2 ∥ VtxDeg (X) (U))$
17	16	notbid	$⊢ x = U \to (\neg 2 ∥ VtxDeg (X) (x) \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
18	17	elrab3	$⊢ U \in V \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
19	5 18	syl	$⊢ φ \to (U \in \{x \in V \| \neg 2 ∥ VtxDeg (X) (x)\} \leftrightarrow \neg 2 ∥ VtxDeg (X) (U))$
20	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)\}))$
21	19 20	bitr3d	$⊢ φ \to (\neg 2 ∥ VtxDeg (X) (U) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
22	21	adantr	$⊢ (φ \land P (N) = P (N + 1)) \to (\neg 2 ∥ VtxDeg (X) (U) \leftrightarrow U \in if (P (0) = P (N), \emptyset, \{P (0), P (N)\}))$
23		2z	$⊢ 2 \in ℤ$
24	23	a1i	$⊢ (φ \land P (N) = P (N + 1)) \to 2 \in ℤ$
25	1 2 3 4 5 6 7 8 9 10 11 12	eupth2lem3lem1	$⊢ φ \to VtxDeg (X) (U) \in ℕ_{0}$
26	25	nn0zd	$⊢ φ \to VtxDeg (X) (U) \in ℤ$
27	26	adantr	$⊢ (φ \land P (N) = P (N + 1)) \to VtxDeg (X) (U) \in ℤ$
28	1 2 3 4 5 6 7 8 9 10 11 12	eupth2lem3lem2	$⊢ φ \to VtxDeg (Y) (U) \in ℕ_{0}$
29	28	nn0zd	$⊢ φ \to VtxDeg (Y) (U) \in ℤ$
30	29	adantr	$⊢ (φ \land P (N) = P (N + 1)) \to VtxDeg (Y) (U) \in ℤ$
31		z2even	$⊢ 2 ∥ 2$
32	8	ad2antrr	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to Vtx (Y) = V$
33		fvexd	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to F (N) \in V$
34	5	ad2antrr	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to U \in V$
35	11	ad2antrr	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
36	14	adantr	$⊢ (φ \land 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)))$
37		ifptru	$⊢ 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 I (F (N)) = \{P (N)\})$
38	37	adantl	$⊢ (φ \land 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 I (F (N)) = \{P (N)\})$
39	36 38	mpbid	$⊢ (φ \land P (N) = P (N + 1)) \to I (F (N)) = \{P (N)\}$
40		sneq	$⊢ P (N) = U \to \{P (N)\} = \{U\}$
41	40	eqcoms	$⊢ U = P (N) \to \{P (N)\} = \{U\}$
42	39 41	sylan9eq	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to I (F (N)) = \{U\}$
43	42	opeq2d	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to ⟨F (N), I (F (N))⟩ = ⟨F (N), \{U\}⟩$
44	43	sneqd	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to \{⟨F (N), I (F (N))⟩\} = \{⟨F (N), \{U\}⟩\}$
45	35 44	eqtrd	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to iEdg (Y) = \{⟨F (N), \{U\}⟩\}$
46	32 33 34 45	1loopgrvd2	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to VtxDeg (Y) (U) = 2$
47	31 46	breqtrrid	$⊢ ((φ \land P (N) = P (N + 1)) \land U = P (N)) \to 2 ∥ VtxDeg (Y) (U)$
48		z0even	$⊢ 2 ∥ 0$
49	8	ad2antrr	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to Vtx (Y) = V$
50		fvexd	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to F (N) \in V$
51	1 2 3 4 5 6	trlsegvdeglem1	$⊢ φ \to (P (N) \in V \land P (N + 1) \in V)$
52	51	simpld	$⊢ φ \to P (N) \in V$
53	52	ad2antrr	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to P (N) \in V$
54	11	adantr	$⊢ (φ \land P (N) = P (N + 1)) \to iEdg (Y) = \{⟨F (N), I (F (N))⟩\}$
55	39	opeq2d	$⊢ (φ \land P (N) = P (N + 1)) \to ⟨F (N), I (F (N))⟩ = ⟨F (N), \{P (N)\}⟩$
56	55	sneqd	$⊢ (φ \land P (N) = P (N + 1)) \to \{⟨F (N), I (F (N))⟩\} = \{⟨F (N), \{P (N)\}⟩\}$
57	54 56	eqtrd	$⊢ (φ \land P (N) = P (N + 1)) \to iEdg (Y) = \{⟨F (N), \{P (N)\}⟩\}$
58	57	adantr	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to iEdg (Y) = \{⟨F (N), \{P (N)\}⟩\}$
59	5	adantr	$⊢ (φ \land P (N) = P (N + 1)) \to U \in V$
60	59	anim1i	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to (U \in V \land U \neq P (N))$
61		eldifsn	$⊢ U \in (V ∖ \{P (N)\}) \leftrightarrow (U \in V \land U \neq P (N))$
62	60 61	sylibr	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to U \in (V ∖ \{P (N)\})$
63	49 50 53 58 62	1loopgrvd0	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to VtxDeg (Y) (U) = 0$
64	48 63	breqtrrid	$⊢ ((φ \land P (N) = P (N + 1)) \land U \neq P (N)) \to 2 ∥ VtxDeg (Y) (U)$
65	47 64	pm2.61dane	$⊢ (φ \land P (N) = P (N + 1)) \to 2 ∥ VtxDeg (Y) (U)$
66		dvdsadd2b	$⊢ (2 \in ℤ \land VtxDeg (X) (U) \in ℤ \land (VtxDeg (Y) (U) \in ℤ \land 2 ∥ VtxDeg (Y) (U))) \to (2 ∥ VtxDeg (X) (U) \leftrightarrow 2 ∥ (VtxDeg (Y) (U) + VtxDeg (X) (U)))$
67	24 27 30 65 66	syl112anc	$⊢ (φ \land P (N) = P (N + 1)) \to (2 ∥ VtxDeg (X) (U) \leftrightarrow 2 ∥ (VtxDeg (Y) (U) + VtxDeg (X) (U)))$
68	28	nn0cnd	$⊢ φ \to VtxDeg (Y) (U) \in ℂ$
69	25	nn0cnd	$⊢ φ \to VtxDeg (X) (U) \in ℂ$
70	68 69	addcomd	$⊢ φ \to VtxDeg (Y) (U) + VtxDeg (X) (U) = VtxDeg (X) (U) + VtxDeg (Y) (U)$
71	70	breq2d	$⊢ φ \to (2 ∥ (VtxDeg (Y) (U) + VtxDeg (X) (U)) \leftrightarrow 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)))$
72	71	adantr	$⊢ (φ \land P (N) = P (N + 1)) \to (2 ∥ (VtxDeg (Y) (U) + VtxDeg (X) (U)) \leftrightarrow 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)))$
73	67 72	bitrd	$⊢ (φ \land P (N) = P (N + 1)) \to (2 ∥ VtxDeg (X) (U) \leftrightarrow 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)))$
74	73	notbid	$⊢ (φ \land P (N) = P (N + 1)) \to (\neg 2 ∥ VtxDeg (X) (U) \leftrightarrow \neg 2 ∥ (VtxDeg (X) (U) + VtxDeg (Y) (U)))$
75		simpr	$⊢ (φ \land P (N) = P (N + 1)) \to P (N) = P (N + 1)$
76	75	eqeq2d	$⊢ (φ \land P (N) = P (N + 1)) \to (P (0) = P (N) \leftrightarrow P (0) = P (N + 1))$
77	75	preq2d	$⊢ (φ \land P (N) = P (N + 1)) \to \{P (0), P (N)\} = \{P (0), P (N + 1)\}$
78	76 77	ifbieq2d	$⊢ (φ \land P (N) = P (N + 1)) \to if (P (0) = P (N), \emptyset, \{P (0), P (N)\}) = if (P (0) = P (N + 1), \emptyset, \{P (0), P (N + 1)\})$
79	78	eleq2d	$⊢ (φ \land P (N) = 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)\}))$
80	22 74 79	3bitr3d	$⊢ (φ \land P (N) = 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 eupth2lem3lem3

Proof