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