Metamath Proof Explorer


Theorem finsumvtxdg2ssteplem2

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 finsumvtxdg2ssteplem2 ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸𝑖 ) = { 𝑁 } } ) ) )

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 dmfi ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin )
9 8 adantl ( ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) → dom 𝐸 ∈ Fin )
10 simpr ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) → 𝑁𝑉 )
11 eqid dom 𝐸 = dom 𝐸
12 1 2 11 vtxdgfival ( ( dom 𝐸 ∈ Fin ∧ 𝑁𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸𝑖 ) = { 𝑁 } } ) ) )
13 9 10 12 syl2anr ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸𝑖 ) = { 𝑁 } } ) ) )
14 7 eqcomi { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } = 𝐽
15 14 fveq2i ( ♯ ‘ { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } ) = ( ♯ ‘ 𝐽 )
16 15 a1i ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ♯ ‘ { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } ) = ( ♯ ‘ 𝐽 ) )
17 16 oveq1d ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( ♯ ‘ { 𝑖 ∈ dom 𝐸𝑁 ∈ ( 𝐸𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸𝑖 ) = { 𝑁 } } ) ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸𝑖 ) = { 𝑁 } } ) ) )
18 13 17 eqtrd ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ 𝐽 ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸𝑖 ) = { 𝑁 } } ) ) )