Theorem vtxdginducedm1fi

Description: The degree of a vertex v in the induced subgraph S of a pseudograph G of finite size 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, 18-Dec-2021)

	Ref	Expression
Hypotheses	vtxdginducedm1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdginducedm1.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
	vtxdginducedm1.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
	vtxdginducedm1.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
	vtxdginducedm1.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
	vtxdginducedm1.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
	vtxdginducedm1.j	⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
Assertion	vtxdginducedm1fi	⊢ ( 𝐸 ∈ Fin → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdginducedm1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdginducedm1.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		vtxdginducedm1.k	⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } )
4		vtxdginducedm1.i	⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) }
5		vtxdginducedm1.p	⊢ 𝑃 = ( 𝐸 ↾ 𝐼 )
6		vtxdginducedm1.s	⊢ 𝑆 = ⟨ 𝐾 , 𝑃 ⟩
7		vtxdginducedm1.j	⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) }
8	1 2 3 4 5 6 7	vtxdginducedm1	⊢ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) )
9	5	dmeqi	⊢ dom 𝑃 = dom ( 𝐸 ↾ 𝐼 )
10		finresfin	⊢ ( 𝐸 ∈ Fin → ( 𝐸 ↾ 𝐼 ) ∈ Fin )
11		dmfi	⊢ ( ( 𝐸 ↾ 𝐼 ) ∈ Fin → dom ( 𝐸 ↾ 𝐼 ) ∈ Fin )
12	10 11	syl	⊢ ( 𝐸 ∈ Fin → dom ( 𝐸 ↾ 𝐼 ) ∈ Fin )
13	9 12	eqeltrid	⊢ ( 𝐸 ∈ Fin → dom 𝑃 ∈ Fin )
14	6	fveq2i	⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ⟨ 𝐾 , 𝑃 ⟩ )
15	1	fvexi	⊢ 𝑉 ∈ V
16	15	difexi	⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V
17	3 16	eqeltri	⊢ 𝐾 ∈ V
18	2	fvexi	⊢ 𝐸 ∈ V
19	18	resex	⊢ ( 𝐸 ↾ 𝐼 ) ∈ V
20	5 19	eqeltri	⊢ 𝑃 ∈ V
21	17 20	opvtxfvi	⊢ ( Vtx ‘ ⟨ 𝐾 , 𝑃 ⟩ ) = 𝐾
22	14 21 3	3eqtrri	⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
23	1 2 3 4 5 6	vtxdginducedm1lem1	⊢ ( iEdg ‘ 𝑆 ) = 𝑃
24	23	eqcomi	⊢ 𝑃 = ( iEdg ‘ 𝑆 )
25		eqid	⊢ dom 𝑃 = dom 𝑃
26	22 24 25	vtxdgfisnn0	⊢ ( ( dom 𝑃 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℕ0 )
27	13 26	sylan	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℕ0 )
28	27	nn0red	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) ∈ ℝ )
29		dmfi	⊢ ( 𝐸 ∈ Fin → dom 𝐸 ∈ Fin )
30		rabfi	⊢ ( dom 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin )
31	29 30	syl	⊢ ( 𝐸 ∈ Fin → { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } ∈ Fin )
32	7 31	eqeltrid	⊢ ( 𝐸 ∈ Fin → 𝐽 ∈ Fin )
33		rabfi	⊢ ( 𝐽 ∈ Fin → { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ∈ Fin )
34		hashcl	⊢ ( { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ∈ Fin → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℕ0 )
35	32 33 34	3syl	⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℕ0 )
36	35	adantr	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℕ0 )
37	36	nn0red	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ∈ ℝ )
38	28 37	rexaddd	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )
39	38	eqeq2d	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) )
40	39	biimpd	⊢ ( ( 𝐸 ∈ Fin ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) )
41	40	ralimdva	⊢ ( 𝐸 ∈ Fin → ( ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) +𝑒 ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) ) )
42	8 41	mpi	⊢ ( 𝐸 ∈ Fin → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ( VtxDeg ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙 ∈ 𝐽 ∣ 𝑣 ∈ ( 𝐸 ‘ 𝑙 ) } ) ) )