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 ⊢ 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 vtxdginducedm1fi ⊢ E ∈ Fin → ∀ 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 1 2 3 4 5 6 7 vtxdginducedm1 ⊢ ∀ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + 𝑒 l ∈ J | v ∈ E ⁡ l
9 5 dmeqi ⊢ dom ⁡ P = dom ⁡ E ↾ I
10 finresfin ⊢ E ∈ Fin → E ↾ I ∈ Fin
11 dmfi ⊢ E ↾ I ∈ Fin → dom ⁡ E ↾ I ∈ Fin
12 10 11 syl ⊢ E ∈ Fin → dom ⁡ E ↾ I ∈ Fin
13 9 12 eqeltrid ⊢ E ∈ Fin → dom ⁡ P ∈ Fin
14 6 fveq2i ⊢ Vtx ⁡ S = Vtx ⁡ K P
15 1 fvexi ⊢ V ∈ V
16 15 difexi ⊢ V ∖ N ∈ V
17 3 16 eqeltri ⊢ K ∈ V
18 2 fvexi ⊢ E ∈ V
19 18 resex ⊢ E ↾ I ∈ V
20 5 19 eqeltri ⊢ P ∈ V
21 17 20 opvtxfvi ⊢ Vtx ⁡ K P = K
22 14 21 3 3eqtrri ⊢ V ∖ N = Vtx ⁡ S
23 1 2 3 4 5 6 vtxdginducedm1lem1 ⊢ iEdg ⁡ S = P
24 23 eqcomi ⊢ P = iEdg ⁡ S
25 eqid ⊢ dom ⁡ P = dom ⁡ P
26 22 24 25 vtxdgfisnn0 ⊢ dom ⁡ P ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ S ⁡ v ∈ ℕ 0
27 13 26 sylan ⊢ E ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ S ⁡ v ∈ ℕ 0
28 27 nn0red ⊢ E ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ S ⁡ v ∈ ℝ
29 dmfi ⊢ E ∈ Fin → dom ⁡ E ∈ Fin
30 rabfi ⊢ dom ⁡ E ∈ Fin → i ∈ dom ⁡ E | N ∈ E ⁡ i ∈ Fin
31 29 30 syl ⊢ E ∈ Fin → i ∈ dom ⁡ E | N ∈ E ⁡ i ∈ Fin
32 7 31 eqeltrid ⊢ E ∈ Fin → J ∈ Fin
33 rabfi ⊢ J ∈ Fin → l ∈ J | v ∈ E ⁡ l ∈ Fin
34 hashcl ⊢ l ∈ J | v ∈ E ⁡ l ∈ Fin → l ∈ J | v ∈ E ⁡ l ∈ ℕ 0
35 32 33 34 3syl ⊢ E ∈ Fin → l ∈ J | v ∈ E ⁡ l ∈ ℕ 0
36 35 adantr ⊢ E ∈ Fin ∧ v ∈ V ∖ N → l ∈ J | v ∈ E ⁡ l ∈ ℕ 0
37 36 nn0red ⊢ E ∈ Fin ∧ v ∈ V ∖ N → l ∈ J | v ∈ E ⁡ l ∈ ℝ
38 28 37 rexaddd ⊢ E ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ S ⁡ v + 𝑒 l ∈ J | v ∈ E ⁡ l = VtxDeg ⁡ S ⁡ v + l ∈ J | v ∈ E ⁡ l
39 38 eqeq2d ⊢ E ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + 𝑒 l ∈ J | v ∈ E ⁡ l ↔ VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + l ∈ J | v ∈ E ⁡ l
40 39 biimpd ⊢ E ∈ Fin ∧ v ∈ V ∖ N → VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + 𝑒 l ∈ J | v ∈ E ⁡ l → VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + l ∈ J | v ∈ E ⁡ l
41 40 ralimdva ⊢ E ∈ Fin → ∀ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + 𝑒 l ∈ J | v ∈ E ⁡ l → ∀ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + l ∈ J | v ∈ E ⁡ l
42 8 41 mpi ⊢ E ∈ Fin → ∀ v ∈ V ∖ N VtxDeg ⁡ G ⁡ v = VtxDeg ⁡ S ⁡ v + l ∈ J | v ∈ E ⁡ l