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	|- V = ( Vtx ` G )
	vtxdgval.i	|- I = ( iEdg ` G )
	vtxdgval.a	|- A = dom I
Assertion	vtxdgfival	|- ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) )

Proof

Step	Hyp	Ref	Expression
1		vtxdgval.v	|- V = ( Vtx ` G )
2		vtxdgval.i	|- I = ( iEdg ` G )
3		vtxdgval.a	|- A = dom I
4	1 2 3	vtxdgval	|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
5	4	adantl	|- ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
6		rabfi	|- ( A e. Fin -> { x e. A | U e. ( I ` x ) } e. Fin )
7		hashcl	|- ( { x e. A | U e. ( I ` x ) } e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0 )
8	6 7	syl	|- ( A e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0 )
9	8	nn0red	|- ( A e. Fin -> ( # ` { x e. A | U e. ( I ` x ) } ) e. RR )
10		rabfi	|- ( A e. Fin -> { x e. A | ( I ` x ) = { U } } e. Fin )
11		hashcl	|- ( { x e. A | ( I ` x ) = { U } } e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. NN0 )
12	10 11	syl	|- ( A e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. NN0 )
13	12	nn0red	|- ( A e. Fin -> ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR )
14	9 13	jca	|- ( A e. Fin -> ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR /\ ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) )
15	14	adantr	|- ( ( A e. Fin /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR /\ ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) )
16		rexadd	|- ( ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR /\ ( # ` { x e. A | ( I ` x ) = { U } } ) e. RR ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
17	15 16	syl	|- ( ( A e. Fin /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
18	5 17	eqtrd	|- ( ( A e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) + ( # ` { x e. A | ( I ` x ) = { U } } ) ) )