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