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 = K P
finsumvtxdg2ssteplem.j ⊢ J = i ∈ dom ⁡ E | N ∈ E ⁡ i
Assertion finsumvtxdg2ssteplem3 ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ 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 = K P
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 ∖ N i ∈ J | v ∈ E ⁡ i = ∑ v ∈ V ∖ N i ∈ dom ⁡ E | N ∈ E ⁡ i ∧ v ∈ E ⁡ i
16 15 oveq1d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N = ∑ v ∈ V ∖ N i ∈ 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 ∖ N i ∈ 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 ∖ N i ∈ 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 ∖ N i ∈ 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 ∖ N i ∈ J | v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N = J