Metamath Proof Explorer

Theorem vtxdlfgrval

Description: The value of the vertex degree function for a loop-free graph G . (Contributed by AV, 23-Feb-2021)

Ref Expression
Hypotheses vtxdlfgrval.v ⊢ V = Vtx ⁡ G
vtxdlfgrval.i ⊢ I = iEdg ⁡ G
vtxdlfgrval.a ⊢ A = dom ⁡ I
vtxdlfgrval.d ⊢ D = VtxDeg ⁡ G
Assertion vtxdlfgrval ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → D ⁡ U = x ∈ A | U ∈ I ⁡ x

Proof

Step Hyp Ref Expression
1 vtxdlfgrval.v ⊢ V = Vtx ⁡ G
2 vtxdlfgrval.i ⊢ I = iEdg ⁡ G
3 vtxdlfgrval.a ⊢ A = dom ⁡ I
4 vtxdlfgrval.d ⊢ D = VtxDeg ⁡ G
5 4 fveq1i ⊢ D ⁡ U = VtxDeg ⁡ G ⁡ U
6 1 2 3 vtxdgval ⊢ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U
7 6 adantl ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U
8 5 7 syl5eq ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → D ⁡ U = x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U
9 eqid ⊢ x ∈ 𝒫 V | 2 ≤ x = x ∈ 𝒫 V | 2 ≤ x
10 2 3 9 lfgrnloop ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x → x ∈ A | I ⁡ x = U = ∅
11 10 adantr ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → x ∈ A | I ⁡ x = U = ∅
12 11 fveq2d ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → x ∈ A | I ⁡ x = U = ∅
13 hash0 ⊢ ∅ = 0
14 12 13 eqtrdi ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → x ∈ A | I ⁡ x = U = 0
15 14 oveq2d ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → x ∈ A | U ∈ I ⁡ x + 𝑒 x ∈ A | I ⁡ x = U = x ∈ A | U ∈ I ⁡ x + 𝑒 0
16 2 dmeqi ⊢ dom ⁡ I = dom ⁡ iEdg ⁡ G
17 3 16 eqtri ⊢ A = dom ⁡ iEdg ⁡ G
18 fvex ⊢ iEdg ⁡ G ∈ V
19 18 dmex ⊢ dom ⁡ iEdg ⁡ G ∈ V
20 17 19 eqeltri ⊢ A ∈ V
21 20 rabex ⊢ x ∈ A | U ∈ I ⁡ x ∈ V
22 hashxnn0 ⊢ x ∈ A | U ∈ I ⁡ x ∈ V → x ∈ A | U ∈ I ⁡ x ∈ ℕ 0 *
23 xnn0xr ⊢ x ∈ A | U ∈ I ⁡ x ∈ ℕ 0 * → x ∈ A | U ∈ I ⁡ x ∈ ℝ *
24 21 22 23 mp2b ⊢ x ∈ A | U ∈ I ⁡ x ∈ ℝ *
25 xaddid1 ⊢ x ∈ A | U ∈ I ⁡ x ∈ ℝ * → x ∈ A | U ∈ I ⁡ x + 𝑒 0 = x ∈ A | U ∈ I ⁡ x
26 24 25 mp1i ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → x ∈ A | U ∈ I ⁡ x + 𝑒 0 = x ∈ A | U ∈ I ⁡ x
27 8 15 26 3eqtrd ⊢ I : A ⟶ x ∈ 𝒫 V | 2 ≤ x ∧ U ∈ V → D ⁡ U = x ∈ A | U ∈ I ⁡ x