Metamath Proof Explorer

Theorem finsumvtxdg2ssteplem4

Description: Lemma for finsumvtxdg2sstep . (Contributed by AV, 12-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 finsumvtxdg2ssteplem4 ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ 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 1 2 3 4 5 6 7 vtxdginducedm1fi ⊢ E ∈ Fin → ∀ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + i ∈ J | v ∈ E ⁡ i
9 8 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∀ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + i ∈ J | v ∈ E ⁡ i
10 9 sumeq2d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v + i ∈ J | v ∈ E ⁡ i
11 diffi ⊢ V ∈ Fin → V ∖ N ∈ Fin
12 11 adantr ⊢ V ∈ Fin ∧ E ∈ Fin → V ∖ N ∈ Fin
13 12 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → V ∖ N ∈ Fin
14 5 dmeqi ⊢ dom ⁡ P = dom ⁡ E ↾ I
15 finresfin ⊢ E ∈ Fin → E ↾ I ∈ Fin
16 dmfi ⊢ E ↾ I ∈ Fin → dom ⁡ E ↾ I ∈ Fin
17 15 16 syl ⊢ E ∈ Fin → dom ⁡ E ↾ I ∈ Fin
18 14 17 eqeltrid ⊢ E ∈ Fin → dom ⁡ P ∈ Fin
19 18 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → dom ⁡ P ∈ Fin
20 3 eqcomi ⊢ V ∖ N = K
21 20 eleq2i ⊢ v ∈ V ∖ N ↔ v ∈ K
22 21 biimpi ⊢ v ∈ V ∖ N → v ∈ K
23 6 fveq2i ⊢ Vtx ⁡ S = Vtx ⁡ K P
24 1 fvexi ⊢ V ∈ V
25 24 difexi ⊢ V ∖ N ∈ V
26 3 25 eqeltri ⊢ K ∈ V
27 2 fvexi ⊢ E ∈ V
28 27 resex ⊢ E ↾ I ∈ V
29 5 28 eqeltri ⊢ P ∈ V
30 26 29 opvtxfvi ⊢ Vtx ⁡ K P = K
31 23 30 eqtr2i ⊢ K = Vtx ⁡ S
32 1 2 3 4 5 6 vtxdginducedm1lem1 ⊢ iEdg ⁡ S = P
33 32 eqcomi ⊢ P = iEdg ⁡ S
34 eqid ⊢ dom ⁡ P = dom ⁡ P
35 31 33 34 vtxdgfisnn0 ⊢ dom ⁡ P ∈ Fin ∧ v ∈ K → VtxDeg ⁡ S ⁡ v ∈ ℕ 0
36 35 nn0cnd ⊢ dom ⁡ P ∈ Fin ∧ v ∈ K → VtxDeg ⁡ S ⁡ v ∈ ℂ
37 19 22 36 syl2an ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ S ⁡ v ∈ ℂ
38 dmfi ⊢ E ∈ Fin → dom ⁡ E ∈ Fin
39 rabfi ⊢ dom ⁡ E ∈ Fin → i ∈ dom ⁡ E | N ∈ E ⁡ i ∈ Fin
40 38 39 syl ⊢ E ∈ Fin → i ∈ dom ⁡ E | N ∈ E ⁡ i ∈ Fin
41 7 40 eqeltrid ⊢ E ∈ Fin → J ∈ Fin
42 rabfi ⊢ J ∈ Fin → i ∈ J | v ∈ E ⁡ i ∈ Fin
43 hashcl ⊢ i ∈ J | v ∈ E ⁡ i ∈ Fin → i ∈ J | v ∈ E ⁡ i ∈ ℕ 0
44 41 42 43 3syl ⊢ E ∈ Fin → i ∈ J | v ∈ E ⁡ i ∈ ℕ 0
45 44 nn0cnd ⊢ E ∈ Fin → i ∈ J | v ∈ E ⁡ i ∈ ℂ
46 45 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → i ∈ J | v ∈ E ⁡ i ∈ ℂ
47 46 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ v ∈ V ∖ N → i ∈ J | v ∈ E ⁡ i ∈ ℂ
48 13 37 47 fsumadd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v + i ∈ J | v ∈ E ⁡ i = ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i
49 10 48 eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i
50 3 sumeq1i ⊢ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v
51 50 eqeq1i ⊢ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P ↔ ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v = 2 ⁢ P
52 oveq1 ⊢ ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i = 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i
53 51 52 sylbi ⊢ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ S ⁡ v + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i = 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i
54 49 53 sylan9eq ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i
55 54 oveq1d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N
56 45 adantl ⊢ V ∈ Fin ∧ E ∈ Fin → i ∈ J | v ∈ E ⁡ i ∈ ℂ
57 56 adantr ⊢ V ∈ Fin ∧ E ∈ Fin ∧ v ∈ V ∖ N → i ∈ J | v ∈ E ⁡ i ∈ ℂ
58 12 57 fsumcl ⊢ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i ∈ ℂ
59 hashcl ⊢ J ∈ Fin → J ∈ ℕ 0
60 41 59 syl ⊢ E ∈ Fin → J ∈ ℕ 0
61 60 nn0cnd ⊢ E ∈ Fin → J ∈ ℂ
62 61 adantl ⊢ V ∈ Fin ∧ E ∈ Fin → J ∈ ℂ
63 rabfi ⊢ dom ⁡ E ∈ Fin → i ∈ dom ⁡ E | E ⁡ i = N ∈ Fin
64 hashcl ⊢ i ∈ dom ⁡ E | E ⁡ i = N ∈ Fin → i ∈ dom ⁡ E | E ⁡ i = N ∈ ℕ 0
65 38 63 64 3syl ⊢ E ∈ Fin → i ∈ dom ⁡ E | E ⁡ i = N ∈ ℕ 0
66 65 nn0cnd ⊢ E ∈ Fin → i ∈ dom ⁡ E | E ⁡ i = N ∈ ℂ
67 66 adantl ⊢ V ∈ Fin ∧ E ∈ Fin → i ∈ dom ⁡ E | E ⁡ i = N ∈ ℂ
68 58 62 67 add12d ⊢ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = J + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N
69 68 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = J + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N
70 1 2 3 4 5 6 7 finsumvtxdg2ssteplem3 ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N = J
71 70 oveq2d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → J + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + i ∈ dom ⁡ E | E ⁡ i = N = J + J
72 61 2timesd ⊢ E ∈ Fin → 2 ⁢ J = J + J
73 72 eqcomd ⊢ E ∈ Fin → J + J = 2 ⁢ J
74 73 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → J + J = 2 ⁢ J
75 69 71 74 3eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ J
76 75 oveq2d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + 2 ⁢ J
77 2cnd ⊢ E ∈ Fin → 2 ∈ ℂ
78 5 15 eqeltrid ⊢ E ∈ Fin → P ∈ Fin
79 hashcl ⊢ P ∈ Fin → P ∈ ℕ 0
80 78 79 syl ⊢ E ∈ Fin → P ∈ ℕ 0
81 80 nn0cnd ⊢ E ∈ Fin → P ∈ ℂ
82 77 81 mulcld ⊢ E ∈ Fin → 2 ⁢ P ∈ ℂ
83 82 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ P ∈ ℂ
84 58 adantl ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i ∈ ℂ
85 61 66 addcld ⊢ E ∈ Fin → J + i ∈ dom ⁡ E | E ⁡ i = N ∈ ℂ
86 85 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → J + i ∈ dom ⁡ E | E ⁡ i = N ∈ ℂ
87 83 84 86 addassd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N
88 2cnd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ∈ ℂ
89 81 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → P ∈ ℂ
90 61 ad2antll ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → J ∈ ℂ
91 88 89 90 adddid ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ P + J = 2 ⁢ P + 2 ⁢ J
92 76 87 91 3eqtr4d ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin → 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + J
93 92 adantr ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → 2 ⁢ P + ∑ v ∈ V ∖ N i ∈ J | v ∈ E ⁡ i + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + J
94 55 93 eqtrd ⊢ G ∈ UPGraph ∧ N ∈ V ∧ V ∈ Fin ∧ E ∈ Fin ∧ ∑ v ∈ K VtxDeg ⁡ S ⁡ v = 2 ⁢ P → ∑ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v + J + i ∈ dom ⁡ E | E ⁡ i = N = 2 ⁢ P + J