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

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 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) )