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 𝑉 = ( Vtx ‘ 𝐺 )
vtxdlfgrval.i 𝐼 = ( iEdg ‘ 𝐺 )
vtxdlfgrval.a 𝐴 = dom 𝐼
vtxdlfgrval.d 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxdlfgrval ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( 𝐷𝑈 ) = ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 vtxdlfgrval.v 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdlfgrval.i 𝐼 = ( iEdg ‘ 𝐺 )
3 vtxdlfgrval.a 𝐴 = dom 𝐼
4 vtxdlfgrval.d 𝐷 = ( VtxDeg ‘ 𝐺 )
5 4 fveq1i ( 𝐷𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 )
6 1 2 3 vtxdgval ( 𝑈𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )
7 6 adantl ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )
8 5 7 syl5eq ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( 𝐷𝑈 ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) )
9 eqid { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
10 2 3 9 lfgrnloop ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } = ∅ )
11 10 adantr ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } = ∅ )
12 11 fveq2d ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) = ( ♯ ‘ ∅ ) )
13 hash0 ( ♯ ‘ ∅ ) = 0
14 12 13 eqtrdi ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) = 0 )
15 14 oveq2d ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥𝐴 ∣ ( 𝐼𝑥 ) = { 𝑈 } } ) ) = ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 0 ) )
16 2 dmeqi dom 𝐼 = dom ( iEdg ‘ 𝐺 )
17 3 16 eqtri 𝐴 = dom ( iEdg ‘ 𝐺 )
18 fvex ( iEdg ‘ 𝐺 ) ∈ V
19 18 dmex dom ( iEdg ‘ 𝐺 ) ∈ V
20 17 19 eqeltri 𝐴 ∈ V
21 20 rabex { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ∈ V
22 hashxnn0 ( { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ∈ V → ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℕ0* )
23 xnn0xr ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℕ0* → ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℝ* )
24 21 22 23 mp2b ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℝ*
25 xaddid1 ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) ∈ ℝ* → ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 0 ) = ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) )
26 24 25 mp1i ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) +𝑒 0 ) = ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) )
27 8 15 26 3eqtrd ( ( 𝐼 : 𝐴 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈𝑉 ) → ( 𝐷𝑈 ) = ( ♯ ‘ { 𝑥𝐴𝑈 ∈ ( 𝐼𝑥 ) } ) )