Metamath Proof Explorer


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 ‘ 𝑆 ) ‘ 𝑣 ) + ( ♯ ‘ { 𝑙𝐽𝑣 ∈ ( 𝐸𝑙 ) } ) ) )