Metamath Proof Explorer


Theorem vtxdginducedm1

Description: The degree of a vertex v in the induced subgraph S of a pseudograph G obtained by removing one vertex N plus the number of edges joining the vertex v and the vertex N is the degree of the vertex v in the pseudograph G . (Contributed by AV, 17-Dec-2021)

Ref Expression
Hypotheses vtxdginducedm1.v V = Vtx G
vtxdginducedm1.e E = iEdg G
vtxdginducedm1.k K = V N
vtxdginducedm1.i I = i dom E | N E i
vtxdginducedm1.p P = E I
vtxdginducedm1.s S = K P
vtxdginducedm1.j J = i dom E | N E i
Assertion vtxdginducedm1 v V N VtxDeg G v = VtxDeg S v + 𝑒 l J | v E l

Proof

Step Hyp Ref Expression
1 vtxdginducedm1.v V = Vtx G
2 vtxdginducedm1.e E = iEdg G
3 vtxdginducedm1.k K = V N
4 vtxdginducedm1.i I = i dom E | N E i
5 vtxdginducedm1.p P = E I
6 vtxdginducedm1.s S = K P
7 vtxdginducedm1.j J = i dom E | N E i
8 7 4 elnelun J I = dom E
9 8 eqcomi dom E = J I
10 9 rabeqi k dom E | v E k = k J I | v E k
11 rabun2 k J I | v E k = k J | v E k k I | v E k
12 10 11 eqtri k dom E | v E k = k J | v E k k I | v E k
13 12 fveq2i k dom E | v E k = k J | v E k k I | v E k
14 2 fvexi E V
15 14 dmex dom E V
16 7 15 rab2ex k J | v E k V
17 4 15 rab2ex k I | v E k V
18 ssrab2 k J | v E k J
19 ssrab2 k I | v E k I
20 ss2in k J | v E k J k I | v E k I k J | v E k k I | v E k J I
21 18 19 20 mp2an k J | v E k k I | v E k J I
22 7 4 elneldisj J I =
23 22 sseq2i k J | v E k k I | v E k J I k J | v E k k I | v E k
24 ss0 k J | v E k k I | v E k k J | v E k k I | v E k =
25 23 24 sylbi k J | v E k k I | v E k J I k J | v E k k I | v E k =
26 21 25 ax-mp k J | v E k k I | v E k =
27 hashunx k J | v E k V k I | v E k V k J | v E k k I | v E k = k J | v E k k I | v E k = k J | v E k + 𝑒 k I | v E k
28 16 17 26 27 mp3an k J | v E k k I | v E k = k J | v E k + 𝑒 k I | v E k
29 13 28 eqtri k dom E | v E k = k J | v E k + 𝑒 k I | v E k
30 9 rabeqi k dom E | E k = v = k J I | E k = v
31 rabun2 k J I | E k = v = k J | E k = v k I | E k = v
32 30 31 eqtri k dom E | E k = v = k J | E k = v k I | E k = v
33 32 fveq2i k dom E | E k = v = k J | E k = v k I | E k = v
34 7 15 rab2ex k J | E k = v V
35 4 15 rab2ex k I | E k = v V
36 ssrab2 k J | E k = v J
37 ssrab2 k I | E k = v I
38 ss2in k J | E k = v J k I | E k = v I k J | E k = v k I | E k = v J I
39 36 37 38 mp2an k J | E k = v k I | E k = v J I
40 22 sseq2i k J | E k = v k I | E k = v J I k J | E k = v k I | E k = v
41 ss0 k J | E k = v k I | E k = v k J | E k = v k I | E k = v =
42 40 41 sylbi k J | E k = v k I | E k = v J I k J | E k = v k I | E k = v =
43 39 42 ax-mp k J | E k = v k I | E k = v =
44 hashunx k J | E k = v V k I | E k = v V k J | E k = v k I | E k = v = k J | E k = v k I | E k = v = k J | E k = v + 𝑒 k I | E k = v
45 34 35 43 44 mp3an k J | E k = v k I | E k = v = k J | E k = v + 𝑒 k I | E k = v
46 33 45 eqtri k dom E | E k = v = k J | E k = v + 𝑒 k I | E k = v
47 29 46 oveq12i k dom E | v E k + 𝑒 k dom E | E k = v = k J | v E k + 𝑒 k I | v E k + 𝑒 k J | E k = v + 𝑒 k I | E k = v
48 hashxnn0 k J | v E k V k J | v E k 0 *
49 16 48 ax-mp k J | v E k 0 *
50 49 a1i v V N k J | v E k 0 *
51 hashxnn0 k I | v E k V k I | v E k 0 *
52 17 51 ax-mp k I | v E k 0 *
53 52 a1i v V N k I | v E k 0 *
54 hashxnn0 k J | E k = v V k J | E k = v 0 *
55 34 54 ax-mp k J | E k = v 0 *
56 55 a1i v V N k J | E k = v 0 *
57 hashxnn0 k I | E k = v V k I | E k = v 0 *
58 35 57 ax-mp k I | E k = v 0 *
59 58 a1i v V N k I | E k = v 0 *
60 50 53 56 59 xnn0add4d v V N k J | v E k + 𝑒 k I | v E k + 𝑒 k J | E k = v + 𝑒 k I | E k = v = k J | v E k + 𝑒 k J | E k = v + 𝑒 k I | v E k + 𝑒 k I | E k = v
61 xnn0xaddcl k J | v E k 0 * k J | E k = v 0 * k J | v E k + 𝑒 k J | E k = v 0 *
62 49 55 61 mp2an k J | v E k + 𝑒 k J | E k = v 0 *
63 xnn0xr k J | v E k + 𝑒 k J | E k = v 0 * k J | v E k + 𝑒 k J | E k = v *
64 62 63 ax-mp k J | v E k + 𝑒 k J | E k = v *
65 xnn0xaddcl k I | v E k 0 * k I | E k = v 0 * k I | v E k + 𝑒 k I | E k = v 0 *
66 52 58 65 mp2an k I | v E k + 𝑒 k I | E k = v 0 *
67 xnn0xr k I | v E k + 𝑒 k I | E k = v 0 * k I | v E k + 𝑒 k I | E k = v *
68 66 67 ax-mp k I | v E k + 𝑒 k I | E k = v *
69 xaddcom k J | v E k + 𝑒 k J | E k = v * k I | v E k + 𝑒 k I | E k = v * k J | v E k + 𝑒 k J | E k = v + 𝑒 k I | v E k + 𝑒 k I | E k = v = k I | v E k + 𝑒 k I | E k = v + 𝑒 k J | v E k + 𝑒 k J | E k = v
70 64 68 69 mp2an k J | v E k + 𝑒 k J | E k = v + 𝑒 k I | v E k + 𝑒 k I | E k = v = k I | v E k + 𝑒 k I | E k = v + 𝑒 k J | v E k + 𝑒 k J | E k = v
71 1 2 3 4 5 6 7 vtxdginducedm1lem4 v V N k J | E k = v = 0
72 71 oveq2d v V N k J | v E k + 𝑒 k J | E k = v = k J | v E k + 𝑒 0
73 xnn0xr k J | v E k 0 * k J | v E k *
74 49 73 ax-mp k J | v E k *
75 xaddid1 k J | v E k * k J | v E k + 𝑒 0 = k J | v E k
76 74 75 ax-mp k J | v E k + 𝑒 0 = k J | v E k
77 72 76 eqtrdi v V N k J | v E k + 𝑒 k J | E k = v = k J | v E k
78 fveq2 k = l E k = E l
79 78 eleq2d k = l v E k v E l
80 79 cbvrabv k J | v E k = l J | v E l
81 80 fveq2i k J | v E k = l J | v E l
82 77 81 eqtrdi v V N k J | v E k + 𝑒 k J | E k = v = l J | v E l
83 82 oveq2d v V N k I | v E k + 𝑒 k I | E k = v + 𝑒 k J | v E k + 𝑒 k J | E k = v = k I | v E k + 𝑒 k I | E k = v + 𝑒 l J | v E l
84 70 83 syl5eq v V N k J | v E k + 𝑒 k J | E k = v + 𝑒 k I | v E k + 𝑒 k I | E k = v = k I | v E k + 𝑒 k I | E k = v + 𝑒 l J | v E l
85 60 84 eqtrd v V N k J | v E k + 𝑒 k I | v E k + 𝑒 k J | E k = v + 𝑒 k I | E k = v = k I | v E k + 𝑒 k I | E k = v + 𝑒 l J | v E l
86 47 85 syl5eq v V N k dom E | v E k + 𝑒 k dom E | E k = v = k I | v E k + 𝑒 k I | E k = v + 𝑒 l J | v E l
87 1 2 3 4 5 6 vtxdginducedm1lem2 dom iEdg S = I
88 87 rabeqi k dom iEdg S | v iEdg S k = k I | v iEdg S k
89 1 2 3 4 5 6 vtxdginducedm1lem3 k I iEdg S k = E k
90 89 eleq2d k I v iEdg S k v E k
91 90 rabbiia k I | v iEdg S k = k I | v E k
92 88 91 eqtri k dom iEdg S | v iEdg S k = k I | v E k
93 92 fveq2i k dom iEdg S | v iEdg S k = k I | v E k
94 87 rabeqi k dom iEdg S | iEdg S k = v = k I | iEdg S k = v
95 89 eqeq1d k I iEdg S k = v E k = v
96 95 rabbiia k I | iEdg S k = v = k I | E k = v
97 94 96 eqtri k dom iEdg S | iEdg S k = v = k I | E k = v
98 97 fveq2i k dom iEdg S | iEdg S k = v = k I | E k = v
99 93 98 oveq12i k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v = k I | v E k + 𝑒 k I | E k = v
100 99 eqcomi k I | v E k + 𝑒 k I | E k = v = k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v
101 100 oveq1i k I | v E k + 𝑒 k I | E k = v + 𝑒 l J | v E l = k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v + 𝑒 l J | v E l
102 86 101 eqtrdi v V N k dom E | v E k + 𝑒 k dom E | E k = v = k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v + 𝑒 l J | v E l
103 eldifi v V N v V
104 eqid dom E = dom E
105 1 2 104 vtxdgval v V VtxDeg G v = k dom E | v E k + 𝑒 k dom E | E k = v
106 103 105 syl v V N VtxDeg G v = k dom E | v E k + 𝑒 k dom E | E k = v
107 6 fveq2i Vtx S = Vtx K P
108 1 fvexi V V
109 difexg V V V N V
110 3 109 eqeltrid V V K V
111 108 110 ax-mp K V
112 resexg E V E I V
113 5 112 eqeltrid E V P V
114 14 113 ax-mp P V
115 111 114 opvtxfvi Vtx K P = K
116 107 115 eqtri Vtx S = K
117 116 eleq2i v Vtx S v K
118 3 eleq2i v K v V N
119 117 118 sylbbr v V N v Vtx S
120 eqid Vtx S = Vtx S
121 eqid iEdg S = iEdg S
122 eqid dom iEdg S = dom iEdg S
123 120 121 122 vtxdgval v Vtx S VtxDeg S v = k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v
124 119 123 syl v V N VtxDeg S v = k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v
125 124 oveq1d v V N VtxDeg S v + 𝑒 l J | v E l = k dom iEdg S | v iEdg S k + 𝑒 k dom iEdg S | iEdg S k = v + 𝑒 l J | v E l
126 102 106 125 3eqtr4d v V N VtxDeg G v = VtxDeg S v + 𝑒 l J | v E l
127 126 rgen v V N VtxDeg G v = VtxDeg S v + 𝑒 l J | v E l