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