Theorem vtxdgfival

Description: The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 21-Jan-2018) (Revised by AV, 8-Dec-2020) (Revised by AV, 22-Mar-2021)

	Ref	Expression
Hypotheses	vtxdgval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	vtxdgval.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	vtxdgval.a	⊢ 𝐴 = dom 𝐼
Assertion	vtxdgfival	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdgval.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		vtxdgval.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		vtxdgval.a	⊢ 𝐴 = dom 𝐼
4	1 2 3	vtxdgval	⊢ ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )
5	4	adantl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )
6		rabfi	⊢ ( 𝐴 ∈ Fin → { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ∈ Fin )
7		hashcl	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℕ0 )
8	6 7	syl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℕ0 )
9	8	nn0red	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ )
10		rabfi	⊢ ( 𝐴 ∈ Fin → { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ∈ Fin )
11		hashcl	⊢ ( { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ∈ ℕ0 )
12	10 11	syl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ∈ ℕ0 )
13	12	nn0red	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ∈ ℝ )
14	9 13	jca	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ ∧ ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ∈ ℝ ) )
15	14	adantr	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ ∧ ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ∈ ℝ ) )
16		rexadd	⊢ ( ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) ∈ ℝ ∧ ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ∈ ℝ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )
17	15 16	syl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )
18	5 17	eqtrd	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑥 ) } ) + ( ♯ ‘ { 𝑥 ∈ 𝐴 ∣ ( 𝐼 ‘ 𝑥 ) = { 𝑈 } } ) ) )