Theorem 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	finsumvtxdg2sstep.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	finsumvtxdg2sstep.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
	finsumvtxdg2sstep.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
	finsumvtxdg2sstep.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
	finsumvtxdg2sstep.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
Assertion	finsumvtxdg2sstep	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( 𝑃 ∈ Fin → Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐸 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdg2sstep.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		finsumvtxdg2sstep.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		finsumvtxdg2sstep.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4		finsumvtxdg2sstep.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
5		finsumvtxdg2sstep.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
6		finsumvtxdg2sstep.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
7		finresfin	⊢ ( 𝐸 ∈ Fin → ( 𝐸 ↾ 𝐼 ) ∈ Fin )
8	7	ad2antll	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 𝐸 ↾ 𝐼 ) ∈ Fin )
9	5 8	eqeltrid	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝑃 ∈ Fin )
10		difsnid	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) = 𝑉 )
11	10	ad2antlr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) = 𝑉 )
12	11	eqcomd	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝑉 = ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) )
13	12	sumeq1d	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = Σ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
14		diffi	⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
15	14	adantr	⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
16	15	adantl	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
17		simpr	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
18	17	adantr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝑁 ∈ 𝑉 )
19		neldifsn	⊢ ¬ 𝑁 ∈ ( 𝑉 ∖ { 𝑁 } )
20	19	nelir	⊢ 𝑁 ∉ ( 𝑉 ∖ { 𝑁 } )
21	20	a1i	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝑁 ∉ ( 𝑉 ∖ { 𝑁 } ) )
22		dmfi	⊢ ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin )
23	22	ad2antll	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → dom 𝐸 ∈ Fin )
24	10	eleq2d	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ↔ 𝑣 ∈ 𝑉 ) )
25	24	biimpd	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) → 𝑣 ∈ 𝑉 ) )
26	25	ad2antlr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) → 𝑣 ∈ 𝑉 ) )
27	26	imp	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ) → 𝑣 ∈ 𝑉 )
28		eqid	⊢ dom 𝐸 = dom 𝐸
29	1 2 28	vtxdgfisnn0	⊢ ( ( dom 𝐸 ∈ Fin ∧ 𝑣 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )
30	23 27 29	syl2an2r	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )
31	30	nn0zd	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℤ )
32	31	ralrimiva	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ∀ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℤ )
33		fsumsplitsnun	⊢ ( ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∉ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ∀ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℤ ) → Σ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ⦋ 𝑁 / 𝑣 ⦌ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ) )
34	16 18 21 32 33	syl121anc	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∪ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ⦋ 𝑁 / 𝑣 ⦌ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ) )
35		fveq2	⊢ ( 𝑣 = 𝑁 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) )
36	35	adantl	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 = 𝑁 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) )
37	17 36	csbied	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ⦋ 𝑁 / 𝑣 ⦌ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) )
38	37	adantr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ⦋ 𝑁 / 𝑣 ⦌ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) )
39	38	oveq2d	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ⦋ 𝑁 / 𝑣 ⦌ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )
40	13 34 39	3eqtrd	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )
41	40	adantr	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) )
42		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝐸 ‘ 𝑗 ) = ( 𝐸 ‘ 𝑖 ) )
43	42	eleq2d	⊢ ( 𝑗 = 𝑖 → ( 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) ↔ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) )
44	43	cbvrabv	⊢ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
45	1 2 3 4 5 6 44	finsumvtxdg2ssteplem2	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) )
46	45	oveq2d	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) )
47	46	adantr	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) )
48	1 2 3 4 5 6 44	finsumvtxdg2ssteplem4	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) ) ) )
49	44	fveq2i	⊢ ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )
50	49	oveq2i	⊢ ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) )
51	50	oveq2i	⊢ ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
52	51	a1i	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑗 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑗 ) } ) ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) ) )
53	47 48 52	3eqtrd	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) ) )
54		eqid	⊢ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
55	1 2 3 4 5 6 54	finsumvtxdg2ssteplem1	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
56	55	oveq2d	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 2 · ( ♯ ‘ 𝐸 ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) ) )
57	56	eqcomd	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) ) = ( 2 · ( ♯ ‘ 𝐸 ) ) )
58	57	adantr	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) ) = ( 2 · ( ♯ ‘ 𝐸 ) ) )
59	41 53 58	3eqtrd	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐸 ) ) )
60	59	ex	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐸 ) ) ) )
61	9 60	embantd	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( 𝑃 ∈ Fin → Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → Σ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐸 ) ) ) )