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 eqtrid ⊢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 xaddrid ⊢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