finsumvtxdg2ssteplem4

	Ref	Expression
Hypotheses	finsumvtxdg2sstep.v	$⊢ V = Vtx (G)$
	finsumvtxdg2sstep.e	$⊢ E = iEdg (G)$
	finsumvtxdg2sstep.k	$⊢ K = V ∖ \{N\}$
	finsumvtxdg2sstep.i	$⊢ I = \{i \in dom E \| N \notin E (i)\}$
	finsumvtxdg2sstep.p	$⊢ P = {E ↾}_{I}$
	finsumvtxdg2sstep.s	$⊢ S = ⟨K, P⟩$
	finsumvtxdg2ssteplem.j	$⊢ J = \{i \in dom E \| N \in E (i)\}$
Assertion	finsumvtxdg2ssteplem4	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 (\|P\| + \|J\|)$

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdg2sstep.v	$⊢ V = Vtx (G)$
2		finsumvtxdg2sstep.e	$⊢ E = iEdg (G)$
3		finsumvtxdg2sstep.k	$⊢ K = V ∖ \{N\}$
4		finsumvtxdg2sstep.i	$⊢ I = \{i \in dom E \| N \notin E (i)\}$
5		finsumvtxdg2sstep.p	$⊢ P = {E ↾}_{I}$
6		finsumvtxdg2sstep.s	$⊢ S = ⟨K, P⟩$
7		finsumvtxdg2ssteplem.j	$⊢ J = \{i \in dom E \| N \in E (i)\}$
8	1 2 3 4 5 6 7	vtxdginducedm1fi	$⊢ E \in Fin \to \forall v \in (V ∖ \{N\}) VtxDeg (G) (v) = VtxDeg (S) (v) + \|\{i \in J \| v \in E (i)\}\|$
9	8	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \forall v \in (V ∖ \{N\}) VtxDeg (G) (v) = VtxDeg (S) (v) + \|\{i \in J \| v \in E (i)\}\|$
10	9	sumeq2d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} (VtxDeg (S) (v) + \|\{i \in J \| v \in E (i)\}\|)$
11		diffi	$⊢ V \in Fin \to V ∖ \{N\} \in Fin$
12	11	adantr	$⊢ (V \in Fin \land E \in Fin) \to V ∖ \{N\} \in Fin$
13	12	adantl	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to V ∖ \{N\} \in Fin$
14	5	dmeqi	$⊢ dom P = dom ({E ↾}_{I})$
15		finresfin	$⊢ E \in Fin \to {E ↾}_{I} \in Fin$
16		dmfi	$⊢ {E ↾}_{I} \in Fin \to dom ({E ↾}_{I}) \in Fin$
17	15 16	syl	$⊢ E \in Fin \to dom ({E ↾}_{I}) \in Fin$
18	14 17	eqeltrid	$⊢ E \in Fin \to dom P \in Fin$
19	18	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to dom P \in Fin$
20	3	eqcomi	$⊢ V ∖ \{N\} = K$
21	20	eleq2i	$⊢ v \in (V ∖ \{N\}) \leftrightarrow v \in K$
22	21	biimpi	$⊢ v \in (V ∖ \{N\}) \to v \in K$
23	6	fveq2i	$⊢ Vtx (S) = Vtx (⟨K, P⟩)$
24	1	fvexi	$⊢ V \in V$
25	24	difexi	$⊢ V ∖ \{N\} \in V$
26	3 25	eqeltri	$⊢ K \in V$
27	2	fvexi	$⊢ E \in V$
28	27	resex	$⊢ {E ↾}_{I} \in V$
29	5 28	eqeltri	$⊢ P \in V$
30	26 29	opvtxfvi	$⊢ Vtx (⟨K, P⟩) = K$
31	23 30	eqtr2i	$⊢ K = Vtx (S)$
32	1 2 3 4 5 6	vtxdginducedm1lem1	$⊢ iEdg (S) = P$
33	32	eqcomi	$⊢ P = iEdg (S)$
34		eqid	$⊢ dom P = dom P$
35	31 33 34	vtxdgfisnn0	$⊢ (dom P \in Fin \land v \in K) \to VtxDeg (S) (v) \in ℕ_{0}$
36	35	nn0cnd	$⊢ (dom P \in Fin \land v \in K) \to VtxDeg (S) (v) \in ℂ$
37	19 22 36	syl2an	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land v \in (V ∖ \{N\})) \to VtxDeg (S) (v) \in ℂ$
38		dmfi	$⊢ E \in Fin \to dom E \in Fin$
39		rabfi	$⊢ dom E \in Fin \to \{i \in dom E \| N \in E (i)\} \in Fin$
40	38 39	syl	$⊢ E \in Fin \to \{i \in dom E \| N \in E (i)\} \in Fin$
41	7 40	eqeltrid	$⊢ E \in Fin \to J \in Fin$
42		rabfi	$⊢ J \in Fin \to \{i \in J \| v \in E (i)\} \in Fin$
43		hashcl	$⊢ \{i \in J \| v \in E (i)\} \in Fin \to \|\{i \in J \| v \in E (i)\}\| \in ℕ_{0}$
44	41 42 43	3syl	$⊢ E \in Fin \to \|\{i \in J \| v \in E (i)\}\| \in ℕ_{0}$
45	44	nn0cnd	$⊢ E \in Fin \to \|\{i \in J \| v \in E (i)\}\| \in ℂ$
46	45	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|\{i \in J \| v \in E (i)\}\| \in ℂ$
47	46	adantr	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land v \in (V ∖ \{N\})) \to \|\{i \in J \| v \in E (i)\}\| \in ℂ$
48	13 37 47	fsumadd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} (VtxDeg (S) (v) + \|\{i \in J \| v \in E (i)\}\|) = \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v) + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\|$
49	10 48	eqtrd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v) + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\|$
50	3	sumeq1i	$⊢ \sum_{v \in K} VtxDeg (S) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v)$
51	50	eqeq1i	$⊢ \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\| \leftrightarrow \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v) = 2 \|P\|$
52		oveq1	$⊢ \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v) = 2 \|P\| \to \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v) + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| = 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\|$
53	51 52	sylbi	$⊢ \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\| \to \sum_{v \in V ∖ \{N\}} VtxDeg (S) (v) + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| = 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\|$
54	49 53	sylan9eq	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) = 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\|$
55	54	oveq1d	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\|$
56	45	adantl	$⊢ (V \in Fin \land E \in Fin) \to \|\{i \in J \| v \in E (i)\}\| \in ℂ$
57	56	adantr	$⊢ ((V \in Fin \land E \in Fin) \land v \in (V ∖ \{N\})) \to \|\{i \in J \| v \in E (i)\}\| \in ℂ$
58	12 57	fsumcl	$⊢ (V \in Fin \land E \in Fin) \to \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| \in ℂ$
59		hashcl	$⊢ J \in Fin \to \|J\| \in ℕ_{0}$
60	41 59	syl	$⊢ E \in Fin \to \|J\| \in ℕ_{0}$
61	60	nn0cnd	$⊢ E \in Fin \to \|J\| \in ℂ$
62	61	adantl	$⊢ (V \in Fin \land E \in Fin) \to \|J\| \in ℂ$
63		rabfi	$⊢ dom E \in Fin \to \{i \in dom E \| E (i) = \{N\}\} \in Fin$
64		hashcl	$⊢ \{i \in dom E \| E (i) = \{N\}\} \in Fin \to \|\{i \in dom E \| E (i) = \{N\}\}\| \in ℕ_{0}$
65	38 63 64	3syl	$⊢ E \in Fin \to \|\{i \in dom E \| E (i) = \{N\}\}\| \in ℕ_{0}$
66	65	nn0cnd	$⊢ E \in Fin \to \|\{i \in dom E \| E (i) = \{N\}\}\| \in ℂ$
67	66	adantl	$⊢ (V \in Fin \land E \in Fin) \to \|\{i \in dom E \| E (i) = \{N\}\}\| \in ℂ$
68	58 62 67	add12d	$⊢ (V \in Fin \land E \in Fin) \to \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = \|J\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\|$
69	68	adantl	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = \|J\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\|$
70	1 2 3 4 5 6 7	finsumvtxdg2ssteplem3	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = \|J\|$
71	70	oveq2d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|J\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = \|J\| + \|J\|$
72	61	2timesd	$⊢ E \in Fin \to 2 \|J\| = \|J\| + \|J\|$
73	72	eqcomd	$⊢ E \in Fin \to \|J\| + \|J\| = 2 \|J\|$
74	73	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|J\| + \|J\| = 2 \|J\|$
75	69 71 74	3eqtrd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 \|J\|$
76	75	oveq2d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + (\|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\|) = 2 \|P\| + 2 \|J\|$
77		2cnd	$⊢ E \in Fin \to 2 \in ℂ$
78	5 15	eqeltrid	$⊢ E \in Fin \to P \in Fin$
79		hashcl	$⊢ P \in Fin \to \|P\| \in ℕ_{0}$
80	78 79	syl	$⊢ E \in Fin \to \|P\| \in ℕ_{0}$
81	80	nn0cnd	$⊢ E \in Fin \to \|P\| \in ℂ$
82	77 81	mulcld	$⊢ E \in Fin \to 2 \|P\| \in ℂ$
83	82	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 \|P\| \in ℂ$
84	58	adantl	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| \in ℂ$
85	61 66	addcld	$⊢ E \in Fin \to \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| \in ℂ$
86	85	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| \in ℂ$
87	83 84 86	addassd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + (\|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\|)$
88		2cnd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 \in ℂ$
89	81	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|P\| \in ℂ$
90	61	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|J\| \in ℂ$
91	88 89 90	adddid	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 (\|P\| + \|J\|) = 2 \|P\| + 2 \|J\|$
92	76 87 91	3eqtr4d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 (\|P\| + \|J\|)$
93	92	adantr	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to 2 \|P\| + \sum_{v \in V ∖ \{N\}} \|\{i \in J \| v \in E (i)\}\| + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 (\|P\| + \|J\|)$
94	55 93	eqtrd	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + \|J\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 (\|P\| + \|J\|)$

Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem4

Proof