Metamath Proof Explorer


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