Metamath Proof Explorer

Theorem finsumvtxdg2sstep

Description: Induction step of finsumvtxdg2size : In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (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
Assertion finsumvtxdg2sstep ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → P ∈ Fin → ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = 2 ⁢ E

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 finresfin ⊢ E ∈ Fin → E ↾ I ∈ Fin
8 7 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → E ↾ I ∈ Fin
9 5 8 eqeltrid ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → P ∈ Fin
10 difsnid ⊢ N ∈ V → V ∖ N ∪ N = V
11 10 ad2antlr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → V ∖ N ∪ N = V
12 11 eqcomd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → V = V ∖ N ∪ N
13 12 sumeq1d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N ∪ N VtxDeg ⁡ G ⁡ v
14 diffi ⊢ V ∈ Fin → V ∖ N ∈ Fin
15 14 adantr ⊢ V ∈ Fin ∧ E ∈ Fin → V ∖ N ∈ Fin
16 15 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → V ∖ N ∈ Fin
17 simpr ⊢ G ∈ UPGraph ∧ N ∈ V → N ∈ V
18 17 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → N ∈ V
19 neldifsn ⊢ ¬ N ∈ V ∖ N
20 19 nelir ⊢ N ∉ V ∖ N
21 20 a1i ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → N ∉ V ∖ N
22 dmfi ⊢ E ∈ Fin → dom ⁡ E ∈ Fin
23 22 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → dom ⁡ E ∈ Fin
24 10 eleq2d ⊢ N ∈ V → v ∈ V ∖ N ∪ N ↔ v ∈ V
25 24 biimpd ⊢ N ∈ V → v ∈ V ∖ N ∪ N → v ∈ V
26 25 ad2antlr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → v ∈ V ∖ N ∪ N → v ∈ V
27 26 imp ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ v ∈ V ∖ N ∪ N → v ∈ V
28 eqid ⊢ dom ⁡ E = dom ⁡ E
29 1 2 28 vtxdgfisnn0 ⊢ dom ⁡ E ∈ Fin ∧ v ∈ V → VtxDeg ⁡ G ⁡ v ∈ ℕ 0
30 23 27 29 syl2an2r ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ v ∈ V ∖ N ∪ N → VtxDeg ⁡ G ⁡ v ∈ ℕ 0
31 30 nn0zd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ v ∈ V ∖ N ∪ N → VtxDeg ⁡ G ⁡ v ∈ ℤ
32 31 ralrimiva ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∀ v ∈ V ∖ N ∪ N VtxDeg ⁡ G ⁡ v ∈ ℤ
33 fsumsplitsnun ⊢ V ∖ N ∈ Fin ∧ N ∈ V ∧ N ∉ V ∖ N ∧ ∀ v ∈ V ∖ N ∪ N VtxDeg ⁡ G ⁡ v ∈ ℤ → ∑ v ∈ V ∖ N ∪ N VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + ⦋ N / v⦌ VtxDeg ⁡ G ⁡ v
34 16 18 21 32 33 syl121anc ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N ∪ N VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + ⦋ N / v⦌ VtxDeg ⁡ G ⁡ v
35 fveq2 ⊢ v = N → VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ G ⁡ N
36 35 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ v = N → VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ G ⁡ N
37 17 36 csbied ⊢ G ∈ UPGraph ∧ N ∈ V → ⦋ N / v⦌ VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ G ⁡ N
38 37 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ⦋ N / v⦌ VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ G ⁡ N
39 38 oveq2d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + ⦋ N / v⦌ VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + VtxDeg ⁡ G ⁡ N
40 13 34 39 3eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + VtxDeg ⁡ G ⁡ N
41 40 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + VtxDeg ⁡ G ⁡ N
42 fveq2 ⊢ j = i → E ⁡ j = E ⁡ i
43 42 eleq2d ⊢ j = i → N ∈ E ⁡ j ↔ N ∈ E ⁡ i
44 43 cbvrabv ⊢ j ∈ dom ⁡ E | N ∈ E ⁡ j = i ∈ dom ⁡ E | N ∈ E ⁡ i
45 1 2 3 4 5 6 44 finsumvtxdg2ssteplem2 ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → VtxDeg ⁡ G ⁡ N = j ∈ dom ⁡ E | N ∈ E ⁡ j + i ∈ dom ⁡ E | E ⁡ i = N
46 45 oveq2d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + VtxDeg ⁡ G ⁡ N = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + j ∈ dom ⁡ E | N ∈ E ⁡ j + i ∈ dom ⁡ E | E ⁡ i = N
47 46 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + VtxDeg ⁡ G ⁡ N = ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + j ∈ dom ⁡ E | N ∈ E ⁡ j + i ∈ dom ⁡ E | E ⁡ i = N
48 1 2 3 4 5 6 44 finsumvtxdg2ssteplem4 ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + j ∈ dom ⁡ E | N ∈ E ⁡ j + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + j ∈ dom ⁡ E | N ∈ E ⁡ j
49 44 fveq2i ⊢ j ∈ dom ⁡ E | N ∈ E ⁡ j = i ∈ dom ⁡ E | N ∈ E ⁡ i
50 49 oveq2i ⊢ P + j ∈ dom ⁡ E | N ∈ E ⁡ j = P + i ∈ dom ⁡ E | N ∈ E ⁡ i
51 50 oveq2i ⊢ 2 ⁢ P + j ∈ dom ⁡ E | N ∈ E ⁡ j = 2 ⁢ P + i ∈ dom ⁡ E | N ∈ E ⁡ i
52 51 a1i ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → 2 ⁢ P + j ∈ dom ⁡ E | N ∈ E ⁡ j = 2 ⁢ P + i ∈ dom ⁡ E | N ∈ E ⁡ i
53 47 48 52 3eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + VtxDeg ⁡ G ⁡ N = 2 ⁢ P + i ∈ dom ⁡ E | N ∈ E ⁡ i
54 eqid ⊢ i ∈ dom ⁡ E | N ∈ E ⁡ i = i ∈ dom ⁡ E | N ∈ E ⁡ i
55 1 2 3 4 5 6 54 finsumvtxdg2ssteplem1 ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → E = P + i ∈ dom ⁡ E | N ∈ E ⁡ i
56 55 oveq2d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ E = 2 ⁢ P + i ∈ dom ⁡ E | N ∈ E ⁡ i
57 56 eqcomd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ P + i ∈ dom ⁡ E | N ∈ E ⁡ i = 2 ⁢ E
58 57 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → 2 ⁢ P + i ∈ dom ⁡ E | N ∈ E ⁡ i = 2 ⁢ E
59 41 53 58 3eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = 2 ⁢ E
60 59 ex ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = 2 ⁢ E
61 9 60 embantd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → P ∈ Fin → ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V VtxDeg ⁡ G ⁡ v = 2 ⁢ E