finsumvtxdg2sstep

Description: Induction step of finsumvtxdg2size : In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (Contributed by AV, 19-Dec-2021)

	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⟩$
Assertion	finsumvtxdg2sstep	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to ((P \in Fin \to \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to \sum_{v \in V} VtxDeg (G) (v) = 2 \|E\|)$

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		finresfin	$⊢ E \in Fin \to {E ↾}_{I} \in Fin$
8	7	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to {E ↾}_{I} \in Fin$
9	5 8	eqeltrid	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to P \in Fin$
10		difsnid	$⊢ N \in V \to (V ∖ \{N\}) \cup \{N\} = V$
11	10	ad2antlr	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to (V ∖ \{N\}) \cup \{N\} = V$
12	11	eqcomd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to V = (V ∖ \{N\}) \cup \{N\}$
13	12	sumeq1d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V} VtxDeg (G) (v) = \sum_{v \in (V ∖ \{N\}) \cup \{N\}} VtxDeg (G) (v)$
14		diffi	$⊢ V \in Fin \to V ∖ \{N\} \in Fin$
15	14	adantr	$⊢ (V \in Fin \land E \in Fin) \to V ∖ \{N\} \in Fin$
16	15	adantl	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to V ∖ \{N\} \in Fin$
17		simpr	$⊢ (G \in UPGraph \land N \in V) \to N \in V$
18	17	adantr	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to N \in V$
19		neldifsn	$⊢ \neg N \in (V ∖ \{N\})$
20	19	nelir	$⊢ N \notin (V ∖ \{N\})$
21	20	a1i	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to N \notin (V ∖ \{N\})$
22		dmfi	$⊢ E \in Fin \to dom E \in Fin$
23	22	ad2antll	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to dom E \in Fin$
24	10	eleq2d	$⊢ N \in V \to (v \in ((V ∖ \{N\}) \cup \{N\}) \leftrightarrow v \in V)$
25	24	biimpd	$⊢ N \in V \to (v \in ((V ∖ \{N\}) \cup \{N\}) \to v \in V)$
26	25	ad2antlr	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to (v \in ((V ∖ \{N\}) \cup \{N\}) \to v \in V)$
27	26	imp	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land v \in ((V ∖ \{N\}) \cup \{N\})) \to v \in V$
28		eqid	$⊢ dom E = dom E$
29	1 2 28	vtxdgfisnn0	$⊢ (dom E \in Fin \land v \in V) \to VtxDeg (G) (v) \in ℕ_{0}$
30	23 27 29	syl2an2r	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land v \in ((V ∖ \{N\}) \cup \{N\})) \to VtxDeg (G) (v) \in ℕ_{0}$
31	30	nn0zd	$⊢ (((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \land v \in ((V ∖ \{N\}) \cup \{N\})) \to VtxDeg (G) (v) \in ℤ$
32	31	ralrimiva	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \forall v \in ((V ∖ \{N\}) \cup \{N\}) VtxDeg (G) (v) \in ℤ$
33		fsumsplitsnun	$⊢ (V ∖ \{N\} \in Fin \land (N \in V \land N \notin (V ∖ \{N\})) \land \forall v \in ((V ∖ \{N\}) \cup \{N\}) VtxDeg (G) (v) \in ℤ) \to \sum_{v \in (V ∖ \{N\}) \cup \{N\}} VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + ⦋ N / v ⦌ VtxDeg (G) (v)$
34	16 18 21 32 33	syl121anc	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in (V ∖ \{N\}) \cup \{N\}} VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + ⦋ N / v ⦌ VtxDeg (G) (v)$
35		fveq2	$⊢ v = N \to VtxDeg (G) (v) = VtxDeg (G) (N)$
36	35	adantl	$⊢ ((G \in UPGraph \land N \in V) \land v = N) \to VtxDeg (G) (v) = VtxDeg (G) (N)$
37	17 36	csbied	$⊢ (G \in UPGraph \land N \in V) \to ⦋ N / v ⦌ VtxDeg (G) (v) = VtxDeg (G) (N)$
38	37	adantr	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to ⦋ N / v ⦌ VtxDeg (G) (v) = VtxDeg (G) (N)$
39	38	oveq2d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + ⦋ N / v ⦌ VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + VtxDeg (G) (N)$
40	13 34 39	3eqtrd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V} VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + VtxDeg (G) (N)$
41	40	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 \sum_{v \in V} VtxDeg (G) (v) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + VtxDeg (G) (N)$
42		fveq2	$⊢ j = i \to E (j) = E (i)$
43	42	eleq2d	$⊢ j = i \to (N \in E (j) \leftrightarrow N \in E (i))$
44	43	cbvrabv	$⊢ \{j \in dom E \| N \in E (j)\} = \{i \in dom E \| N \in E (i)\}$
45	1 2 3 4 5 6 44	finsumvtxdg2ssteplem2	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to VtxDeg (G) (N) = \|\{j \in dom E \| N \in E (j)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\|$
46	45	oveq2d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + VtxDeg (G) (N) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + \|\{j \in dom E \| N \in E (j)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\|$
47	46	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 \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + VtxDeg (G) (N) = \sum_{v \in V ∖ \{N\}} VtxDeg (G) (v) + \|\{j \in dom E \| N \in E (j)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\|$
48	1 2 3 4 5 6 44	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 \in dom E \| N \in E (j)\}\| + \|\{i \in dom E \| E (i) = \{N\}\}\| = 2 (\|P\| + \|\{j \in dom E \| N \in E (j)\}\|)$
49	44	fveq2i	$⊢ \|\{j \in dom E \| N \in E (j)\}\| = \|\{i \in dom E \| N \in E (i)\}\|$
50	49	oveq2i	$⊢ \|P\| + \|\{j \in dom E \| N \in E (j)\}\| = \|P\| + \|\{i \in dom E \| N \in E (i)\}\|$
51	50	oveq2i	$⊢ 2 (\|P\| + \|\{j \in dom E \| N \in E (j)\}\|) = 2 (\|P\| + \|\{i \in dom E \| N \in E (i)\}\|)$
52	51	a1i	$⊢ (((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\| + \|\{j \in dom E \| N \in E (j)\}\|) = 2 (\|P\| + \|\{i \in dom E \| N \in E (i)\}\|)$
53	47 48 52	3eqtrd	$⊢ (((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) + VtxDeg (G) (N) = 2 (\|P\| + \|\{i \in dom E \| N \in E (i)\}\|)$
54		eqid	$⊢ \{i \in dom E \| N \in E (i)\} = \{i \in dom E \| N \in E (i)\}$
55	1 2 3 4 5 6 54	finsumvtxdg2ssteplem1	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to \|E\| = \|P\| + \|\{i \in dom E \| N \in E (i)\}\|$
56	55	oveq2d	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 \|E\| = 2 (\|P\| + \|\{i \in dom E \| N \in E (i)\}\|)$
57	56	eqcomd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to 2 (\|P\| + \|\{i \in dom E \| N \in E (i)\}\|) = 2 \|E\|$
58	57	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\| + \|\{i \in dom E \| N \in E (i)\}\|) = 2 \|E\|$
59	41 53 58	3eqtrd	$⊢ (((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} VtxDeg (G) (v) = 2 \|E\|$
60	59	ex	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to (\sum_{v \in K} VtxDeg (S) (v) = 2 \|P\| \to \sum_{v \in V} VtxDeg (G) (v) = 2 \|E\|)$
61	9 60	embantd	$⊢ ((G \in UPGraph \land N \in V) \land (V \in Fin \land E \in Fin)) \to ((P \in Fin \to \sum_{v \in K} VtxDeg (S) (v) = 2 \|P\|) \to \sum_{v \in V} VtxDeg (G) (v) = 2 \|E\|)$

Metamath Proof Explorer

Theorem finsumvtxdg2sstep

Proof