Theorem finsumvtxdg2ssteplem3

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

	Ref	Expression
Hypotheses	finsumvtxdg2sstep.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	finsumvtxdg2sstep.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	finsumvtxdg2sstep.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
	finsumvtxdg2sstep.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
	finsumvtxdg2sstep.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
	finsumvtxdg2sstep.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
	finsumvtxdg2ssteplem.j	⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
Assertion	finsumvtxdg2ssteplem3	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ 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	7	rabeq2i	⊢ ( 𝑖 ∈ 𝐽 ↔ ( 𝑖 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) )
9	8	anbi1i	⊢ ( ( 𝑖 ∈ 𝐽 ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( ( 𝑖 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) )
10		anass	⊢ ( ( ( 𝑖 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
11	9 10	bitri	⊢ ( ( 𝑖 ∈ 𝐽 ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ↔ ( 𝑖 ∈ dom 𝐸 ∧ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) ) )
12	11	rabbia2	⊢ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } = { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) }
13	12	fveq2i	⊢ ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } )
14	13	a1i	⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) )
15	14	sumeq2dv	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) = Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) )
16	15	oveq1d	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) )
17		simpll	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝐺 ∈ UPGraph )
18		simpr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) )
19		simplr	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → 𝑁 ∈ 𝑉 )
20	1 2	numedglnl	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ∧ 𝑁 ∈ 𝑉 ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) )
21	17 18 19 20	syl3anc	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ∧ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) )
22	16 21	eqtrd	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ) )
23	7	fveq2i	⊢ ( ♯ ‘ 𝐽 ) = ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } )
24	22 23	eqtr4di	⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑉 ∈ Fin ∧ 𝐸 ∈ Fin ) ) → ( Σ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ♯ ‘ { 𝑖 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑖 ) } ) + ( ♯ ‘ { 𝑖 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑖 ) = { 𝑁 } } ) ) = ( ♯ ‘ 𝐽 ) )