trlsegvdeg

Description: Formerly part of proof of eupth2lem3 : If a trail in a graph G induces a subgraph Z with the vertices V of G and the edges being the edges of the walk, and a subgraph X with the vertices V of G and the edges being the edges of the walk except the last one, and a subgraph Y with the vertices V of G and one edges being the last edge of the walk, then the vertex degree of any vertex U of G within Z is the sum of the vertex degree of U within X and the vertex degree of U within Y . Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-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)]}$
Assertion	trlsegvdeg	$⊢ φ \to VtxDeg (Z) (U) = VtxDeg (X) (U) + VtxDeg (Y) (U)$

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		eqid	$⊢ iEdg (X) = iEdg (X)$
14		eqid	$⊢ iEdg (Y) = iEdg (Y)$
15		eqid	$⊢ Vtx (X) = Vtx (X)$
16	8 7	eqtr4d	$⊢ φ \to Vtx (Y) = Vtx (X)$
17	9 7	eqtr4d	$⊢ φ \to Vtx (Z) = Vtx (X)$
18	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem4	$⊢ φ \to dom iEdg (X) = F [(0 ..^N)] \cap dom I$
19	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem5	$⊢ φ \to dom iEdg (Y) = \{F (N)\}$
20	18 19	ineq12d	$⊢ φ \to dom iEdg (X) \cap dom iEdg (Y) = (F [(0 ..^N)] \cap dom I) \cap \{F (N)\}$
21		fzonel	$⊢ \neg N \in (0 ..^N)$
22	2	trlf1	$⊢ F Trails (G) P \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
23	6 22	syl	$⊢ φ \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
24		elfzouz2	$⊢ N \in (0 ..^\|F\|) \to \|F\| \in ℤ_{\geq N}$
25		fzoss2	$⊢ \|F\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|F\|)$
26	4 24 25	3syl	$⊢ φ \to (0 ..^N) \subseteq (0 ..^\|F\|)$
27		f1elima	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land N \in (0 ..^\|F\|) \land (0 ..^N) \subseteq (0 ..^\|F\|)) \to (F (N) \in F [(0 ..^N)] \leftrightarrow N \in (0 ..^N))$
28	23 4 26 27	syl3anc	$⊢ φ \to (F (N) \in F [(0 ..^N)] \leftrightarrow N \in (0 ..^N))$
29	21 28	mtbiri	$⊢ φ \to \neg F (N) \in F [(0 ..^N)]$
30	29	orcd	$⊢ φ \to (\neg F (N) \in F [(0 ..^N)] \lor \neg F (N) \in dom I)$
31		ianor	$⊢ \neg (F (N) \in F [(0 ..^N)] \land F (N) \in dom I) \leftrightarrow (\neg F (N) \in F [(0 ..^N)] \lor \neg F (N) \in dom I)$
32		elin	$⊢ F (N) \in (F [(0 ..^N)] \cap dom I) \leftrightarrow (F (N) \in F [(0 ..^N)] \land F (N) \in dom I)$
33	31 32	xchnxbir	$⊢ \neg F (N) \in (F [(0 ..^N)] \cap dom I) \leftrightarrow (\neg F (N) \in F [(0 ..^N)] \lor \neg F (N) \in dom I)$
34	30 33	sylibr	$⊢ φ \to \neg F (N) \in (F [(0 ..^N)] \cap dom I)$
35		disjsn	$⊢ (F [(0 ..^N)] \cap dom I) \cap \{F (N)\} = \emptyset \leftrightarrow \neg F (N) \in (F [(0 ..^N)] \cap dom I)$
36	34 35	sylibr	$⊢ φ \to (F [(0 ..^N)] \cap dom I) \cap \{F (N)\} = \emptyset$
37	20 36	eqtrd	$⊢ φ \to dom iEdg (X) \cap dom iEdg (Y) = \emptyset$
38	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem2	$⊢ φ \to Fun iEdg (X)$
39	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem3	$⊢ φ \to Fun iEdg (Y)$
40	5 7	eleqtrrd	$⊢ φ \to U \in Vtx (X)$
41		f1f	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \to F : (0 ..^\|F\|) ⟶ dom I$
42	6 22 41	3syl	$⊢ φ \to F : (0 ..^\|F\|) ⟶ dom I$
43	3 42 4	resunimafz0	$⊢ φ \to {I ↾}_{F [(0 \dots N)]} = ({I ↾}_{F [(0 ..^N)]}) \cup \{⟨F (N), I (F (N))⟩\}$
44	10 11	uneq12d	$⊢ φ \to iEdg (X) \cup iEdg (Y) = ({I ↾}_{F [(0 ..^N)]}) \cup \{⟨F (N), I (F (N))⟩\}$
45	43 12 44	3eqtr4d	$⊢ φ \to iEdg (Z) = iEdg (X) \cup iEdg (Y)$
46	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem6	$⊢ φ \to dom iEdg (X) \in Fin$
47	1 2 3 4 5 6 7 8 9 10 11 12	trlsegvdeglem7	$⊢ φ \to dom iEdg (Y) \in Fin$
48	13 14 15 16 17 37 38 39 40 45 46 47	vtxdfiun	$⊢ φ \to VtxDeg (Z) (U) = VtxDeg (X) (U) + VtxDeg (Y) (U)$

Metamath Proof Explorer

Theorem trlsegvdeg

Proof