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

Metamath Proof Explorer

Theorem vtxdgval

Description: The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 10-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	vtxdgval	\|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A \| U e. ( I ` x ) } ) +e ( # ` { 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	1vgrex	\|- ( U e. V -> G e. _V )
5	1 2 3	vtxdgfval	\|- ( G e. _V -> ( VtxDeg ` G ) = ( u e. V \|-> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) ) )
6	4 5	syl	\|- ( U e. V -> ( VtxDeg ` G ) = ( u e. V \|-> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) ) )
7	6	fveq1d	\|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( u e. V \|-> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) ) ` U ) )
8		eleq1	\|- ( u = U -> ( u e. ( I ` x ) <-> U e. ( I ` x ) ) )
9	8	rabbidv	\|- ( u = U -> { x e. A \| u e. ( I ` x ) } = { x e. A \| U e. ( I ` x ) } )
10	9	fveq2d	\|- ( u = U -> ( # ` { x e. A \| u e. ( I ` x ) } ) = ( # ` { x e. A \| U e. ( I ` x ) } ) )
11		sneq	\|- ( u = U -> { u } = { U } )
12	11	eqeq2d	\|- ( u = U -> ( ( I ` x ) = { u } <-> ( I ` x ) = { U } ) )
13	12	rabbidv	\|- ( u = U -> { x e. A \| ( I ` x ) = { u } } = { x e. A \| ( I ` x ) = { U } } )
14	13	fveq2d	\|- ( u = U -> ( # ` { x e. A \| ( I ` x ) = { u } } ) = ( # ` { x e. A \| ( I ` x ) = { U } } ) )
15	10 14	oveq12d	\|- ( u = U -> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) = ( ( # ` { x e. A \| U e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { U } } ) ) )
16		eqid	\|- ( u e. V \|-> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) ) = ( u e. V \|-> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) )
17		ovex	\|- ( ( # ` { x e. A \| U e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { U } } ) ) e. _V
18	15 16 17	fvmpt	\|- ( U e. V -> ( ( u e. V \|-> ( ( # ` { x e. A \| u e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { u } } ) ) ) ` U ) = ( ( # ` { x e. A \| U e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { U } } ) ) )
19	7 18	eqtrd	\|- ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A \| U e. ( I ` x ) } ) +e ( # ` { x e. A \| ( I ` x ) = { U } } ) ) )