Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem1

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 15-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 finsumvtxdg2ssteplem1 ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→E=P+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 upgruhgr ⊢G∈UPGraph→G∈UHGraph
9 2 uhgrfun ⊢G∈UHGraph→Fun⁡E
10 8 9 syl ⊢G∈UPGraph→Fun⁡E
11 10 ad2antrr ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→Fun⁡E
12 simprr ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→E∈Fin
13 4 ssrab3 ⊢I⊆dom⁡E
14 13 a1i ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→I⊆dom⁡E
15 hashreshashfun ⊢Fun⁡E∧E∈Fin∧I⊆dom⁡E→E=E↾I+dom⁡E∖I
16 11 12 14 15 syl3anc ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→E=E↾I+dom⁡E∖I
17 5 eqcomi ⊢E↾I=P
18 17 fveq2i ⊢E↾I=P
19 18 a1i ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→E↾I=P
20 notrab ⊢dom⁡E∖i∈dom⁡E|N∉E⁡i=i∈dom⁡E|¬N∉E⁡i
21 4 difeq2i ⊢dom⁡E∖I=dom⁡E∖i∈dom⁡E|N∉E⁡i
22 nnel ⊢¬N∉E⁡i↔N∈E⁡i
23 22 bicomi ⊢N∈E⁡i↔¬N∉E⁡i
24 23 rabbii ⊢i∈dom⁡E|N∈E⁡i=i∈dom⁡E|¬N∉E⁡i
25 7 24 eqtri ⊢J=i∈dom⁡E|¬N∉E⁡i
26 20 21 25 3eqtr4i ⊢dom⁡E∖I=J
27 26 a1i ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→dom⁡E∖I=J
28 27 fveq2d ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→dom⁡E∖I=J
29 19 28 oveq12d ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→E↾I+dom⁡E∖I=P+J
30 16 29 eqtrd ⊢G∈UPGraph∧N∈V∧V∈Fin∧E∈Fin→E=P+J