This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem4

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 12-Dec-2021)

Ref Expression
Hypotheses finsumvtxdg2sstep.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
finsumvtxdg2sstep.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
finsumvtxdg2sstep.k ⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
finsumvtxdg2sstep.i ⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
finsumvtxdg2sstep.p ⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
finsumvtxdg2sstep.s ⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
finsumvtxdg2ssteplem.j ⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
Assertion finsumvtxdg2ssteplem4 ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( 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 finsumvtxdg2ssteplem.j ⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
8 1 2 3 4 5 6 7 vtxdginducedm1fi ⊢ ( 𝐸 ∈ Fin → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
9 8 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
10 9 sumeq2d ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
11 diffi ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
12 11 adantr ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
13 12 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin )
14 5 dmeqi ⊢ dom 𝑃 = dom ( 𝐸 ↾ 𝐼 )
15 finresfin ⊢ ( 𝐸 ∈ Fin → ( 𝐸 ↾ 𝐼 ) ∈ Fin )
16 dmfi ⊢ ( ( 𝐸 ↾ 𝐼 ) ∈ Fin → dom ( 𝐸 ↾ 𝐼 ) ∈ Fin )
17 15 16 syl ⊢ ( 𝐸 ∈ Fin → dom ( 𝐸 ↾ 𝐼 ) ∈ Fin )
18 14 17 eqeltrid ⊢ ( 𝐸 ∈ Fin → dom 𝑃 ∈ Fin )
19 18 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → dom 𝑃 ∈ Fin )
20 3 eqcomi ⊢ ( 𝑉 ∖ { 𝑁 } ) = 𝐾
21 20 eleq2i ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ 𝑣 ∈ 𝐾 )
22 21 biimpi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑣 ∈ 𝐾 )
23 6 fveq2i ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ⟨ 𝐾 , 𝑃 ⟩ )
24 1 fvexi ⊢ 𝑉 ∈ V
25 24 difexi ⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V
26 3 25 eqeltri ⊢ 𝐾 ∈ V
27 2 fvexi ⊢ 𝐸 ∈ V
28 27 resex ⊢ ( 𝐸 ↾ 𝐼 ) ∈ V
29 5 28 eqeltri ⊢ 𝑃 ∈ V
30 26 29 opvtxfvi ⊢ ( Vtx ‘ ⟨ 𝐾 , 𝑃 ⟩ ) = 𝐾
31 23 30 eqtr2i ⊢ 𝐾 = ( Vtx ‘ 𝑆 )
32 1 2 3 4 5 6 vtxdginducedm1lem1 ⊢ ( iEdg ‘ 𝑆 ) = 𝑃
33 32 eqcomi ⊢ 𝑃 = ( iEdg ‘ 𝑆 )
34 eqid ⊢ dom 𝑃 = dom 𝑃
35 31 33 34 vtxdgfisnn0 ⊢ ( ( dom 𝑃 ∈ Fin ∧ 𝑣 ∈ 𝐾 ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℕ0 )
36 35 nn0cnd ⊢ ( ( dom 𝑃 ∈ Fin ∧ 𝑣 ∈ 𝐾 ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℂ )
37 19 22 36 syl2an ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℂ )
38 dmfi ⊢ ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin )
39 rabfi ⊢ ( dom 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin )
40 38 39 syl ⊢ ( 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin )
41 7 40 eqeltrid ⊢ ( 𝐸 ∈ Fin → 𝐽 ∈ Fin )
42 rabfi ⊢ ( 𝐽 ∈ Fin → { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin )
43 hashcl ⊢ ( { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℕ0 )
44 41 42 43 3syl ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℕ0 )
45 44 nn0cnd ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
46 45 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
47 46 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
48 13 37 47 fsumadd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
49 10 48 eqtrd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
50 3 sumeq1i ⊢ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 )
51 50 eqeq1i ⊢ ( Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ↔ Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) )
52 oveq1 ⊢ ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) = ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
53 51 52 sylbi ⊢ ( Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) = ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
54 49 53 sylan9eq ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) )
55 54 oveq1d ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) )
56 45 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
57 56 adantr ⊢ ( ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
58 12 57 fsumcl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
59 hashcl ⊢ ( 𝐽 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
60 41 59 syl ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
61 60 nn0cnd ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℂ )
62 61 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( ♯ ‘ 𝐽 ) ∈ ℂ )
63 rabfi ⊢ ( dom 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin )
64 hashcl ⊢ ( { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ∈ Fin → ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ∈ ℕ0 )
65 38 63 64 3syl ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ∈ ℕ0 )
66 65 nn0cnd ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ∈ ℂ )
67 66 adantl ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ∈ ℂ )
68 58 62 67 add12d ⊢ ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( ( ♯ ‘ 𝐽 ) + ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) )
69 68 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( ( ♯ ‘ 𝐽 ) + ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) )
70 1 2 3 4 5 6 7 finsumvtxdg2ssteplem3 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ 𝐽 ) )
71 70 oveq2d ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ♯ ‘ 𝐽 ) + ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ 𝐽 ) ) )
72 61 2timesd ⊢ ( 𝐸 ∈ Fin → ( 2 · ( ♯ ‘ 𝐽 ) ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ 𝐽 ) ) )
73 72 eqcomd ⊢ ( 𝐸 ∈ Fin → ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ 𝐽 ) ) = ( 2 · ( ♯ ‘ 𝐽 ) ) )
74 73 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ 𝐽 ) ) = ( 2 · ( ♯ ‘ 𝐽 ) ) )
75 69 71 74 3eqtrd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( 2 · ( ♯ ‘ 𝐽 ) ) )
76 75 oveq2d ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( 2 · ( ♯ ‘ 𝑃 ) ) + ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) ) = ( ( 2 · ( ♯ ‘ 𝑃 ) ) + ( 2 · ( ♯ ‘ 𝐽 ) ) ) )
77 2cnd ⊢ ( 𝐸 ∈ Fin → 2 ∈ ℂ )
78 5 15 eqeltrid ⊢ ( 𝐸 ∈ Fin → 𝑃 ∈ Fin )
79 hashcl ⊢ ( 𝑃 ∈ Fin → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
80 78 79 syl ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
81 80 nn0cnd ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ 𝑃 ) ∈ ℂ )
82 77 81 mulcld ⊢ ( 𝐸 ∈ Fin → ( 2 · ( ♯ ‘ 𝑃 ) ) ∈ ℂ )
83 82 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 2 · ( ♯ ‘ 𝑃 ) ) ∈ ℂ )
84 58 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ∈ ℂ )
85 61 66 addcld ⊢ ( 𝐸 ∈ Fin → ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ∈ ℂ )
86 85 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ∈ ℂ )
87 83 84 86 addassd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( ( 2 · ( ♯ ‘ 𝑃 ) ) + ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) ) )
88 2cnd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 2 ∈ ℂ )
89 81 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ 𝑃 ) ∈ ℂ )
90 61 ad2antll ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ 𝐽 ) ∈ ℂ )
91 88 89 90 adddid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) ) = ( ( 2 · ( ♯ ‘ 𝑃 ) ) + ( 2 · ( ♯ ‘ 𝐽 ) ) ) )
92 76 87 91 3eqtr4d ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) ) )
93 92 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( ( ( 2 · ( ♯ ‘ 𝑃 ) ) + Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) ) )
94 55 93 eqtrd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ Σ 𝑣 ∈ 𝐾 ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝑃 ) ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) + ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) ) = ( 2 · ( ( ♯ ‘ 𝑃 ) + ( ♯ ‘ 𝐽 ) ) ) )