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 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝑈 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑈 ) = ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) )