This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } } ) ) )