Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem3

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

Ref Expression
Hypotheses finsumvtxdg2sstep.v ⊢V=Vtx⁡G
finsumvtxdg2sstep.e ⊢E=iEdg⁡G
finsumvtxdg2sstep.k ⊢K=V∖N
finsumvtxdg2sstep.i ⊢I=i∈dom⁡E|N∉E⁡i
finsumvtxdg2sstep.p ⊢P=E↾I
finsumvtxdg2sstep.s ⊢S=KP
finsumvtxdg2ssteplem.j ⊢J=i∈dom⁡E|N∈E⁡i
Assertion finsumvtxdg2ssteplem3 ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→∑v∈V∖Ni∈J|v∈E⁡i+i∈dom⁡E|E⁡i=N=J

Proof

Step Hyp Ref Expression
1 finsumvtxdg2sstep.v ⊢V=Vtx⁡G
2 finsumvtxdg2sstep.e ⊢E=iEdg⁡G
3 finsumvtxdg2sstep.k ⊢K=V∖N
4 finsumvtxdg2sstep.i ⊢I=i∈dom⁡E|N∉E⁡i
5 finsumvtxdg2sstep.p ⊢P=E↾I
6 finsumvtxdg2sstep.s ⊢S=KP
7 finsumvtxdg2ssteplem.j ⊢J=i∈dom⁡E|N∈E⁡i
8 7 reqabi ⊢i∈J↔i∈dom⁡E∧N∈E⁡i
9 8 anbi1i ⊢i∈J∧v∈E⁡i↔i∈dom⁡E∧N∈E⁡i∧v∈E⁡i
10 anass ⊢i∈dom⁡E∧N∈E⁡i∧v∈E⁡i↔i∈dom⁡E∧N∈E⁡i∧v∈E⁡i
11 9 10 bitri ⊢i∈J∧v∈E⁡i↔i∈dom⁡E∧N∈E⁡i∧v∈E⁡i
12 11 rabbia2 ⊢i∈J|v∈E⁡i=i∈dom⁡E|N∈E⁡i∧v∈E⁡i
13 12 fveq2i ⊢i∈J|v∈E⁡i=i∈dom⁡E|N∈E⁡i∧v∈E⁡i
14 13 a1i ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin∧v∈V∖N→i∈J|v∈E⁡i=i∈dom⁡E|N∈E⁡i∧v∈E⁡i
15 14 sumeq2dv ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→∑v∈V∖Ni∈J|v∈E⁡i=∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i
16 15 oveq1d ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→∑v∈V∖Ni∈J|v∈E⁡i+i∈dom⁡E|E⁡i=N=∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i+i∈dom⁡E|E⁡i=N
17 simpll ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→G∈UPGraph
18 simpr ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→V∈Fin∧E∈Fin
19 simplr ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→N∈V
20 1 2 numedglnl ⊢G∈UPGraph∧V∈Fin∧E∈Fin∧N∈V→∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i+i∈dom⁡E|E⁡i=N=i∈dom⁡E|N∈E⁡i
21 17 18 19 20 syl3anc ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→∑v∈V∖Ni∈dom⁡E|N∈E⁡i∧v∈E⁡i+i∈dom⁡E|E⁡i=N=i∈dom⁡E|N∈E⁡i
22 16 21 eqtrd ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→∑v∈V∖Ni∈J|v∈E⁡i+i∈dom⁡E|E⁡i=N=i∈dom⁡E|N∈E⁡i
23 7 fveq2i ⊢J=i∈dom⁡E|N∈E⁡i
24 22 23 eqtr4di ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→∑v∈V∖Ni∈J|v∈E⁡i+i∈dom⁡E|E⁡i=N=J