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

Metamath Proof Explorer

Theorem vtxdginducedm1

Proof