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 = K P
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 = K P
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