This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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