Metamath Proof Explorer

Theorem vtxdlfgrval

Description: The value of the vertex degree function for a loop-free graph G . (Contributed by AV, 23-Feb-2021)

Ref Expression
Hypotheses vtxdlfgrval.v 
|- V = ( Vtx ` G )
vtxdlfgrval.i 
|- I = ( iEdg ` G )
vtxdlfgrval.a 
|- A = dom I
vtxdlfgrval.d 
|- D = ( VtxDeg ` G )
Assertion vtxdlfgrval 
|- ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )

Proof

Step Hyp Ref Expression
1 vtxdlfgrval.v 
 |-  V = ( Vtx ` G )
2 vtxdlfgrval.i 
 |-  I = ( iEdg ` G )
3 vtxdlfgrval.a 
 |-  A = dom I
4 vtxdlfgrval.d 
 |-  D = ( VtxDeg ` G )
5 4 fveq1i 
 |-  ( D ` U ) = ( ( VtxDeg ` G ) ` U )
6 1 2 3 vtxdgval 
 |-  ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
7 6 adantl 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
8 5 7 syl5eq 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( D ` U ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) )
9 eqid 
 |-  { x e. ~P V | 2 <_ ( # ` x ) } = { x e. ~P V | 2 <_ ( # ` x ) }
10 2 3 9 lfgrnloop 
 |-  ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } -> { x e. A | ( I ` x ) = { U } } = (/) )
11 10 adantr 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> { x e. A | ( I ` x ) = { U } } = (/) )
12 11 fveq2d 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( # ` { x e. A | ( I ` x ) = { U } } ) = ( # ` (/) ) )
13 hash0 
 |-  ( # ` (/) ) = 0
14 12 13 eqtrdi 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( # ` { x e. A | ( I ` x ) = { U } } ) = 0 )
15 14 oveq2d 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { U } } ) ) = ( ( # ` { x e. A | U e. ( I ` x ) } ) +e 0 ) )
16 2 dmeqi 
 |-  dom I = dom ( iEdg ` G )
17 3 16 eqtri 
 |-  A = dom ( iEdg ` G )
18 fvex 
 |-  ( iEdg ` G ) e. _V
19 18 dmex 
 |-  dom ( iEdg ` G ) e. _V
20 17 19 eqeltri 
 |-  A e. _V
21 20 rabex 
 |-  { x e. A | U e. ( I ` x ) } e. _V
22 hashxnn0 
 |-  ( { x e. A | U e. ( I ` x ) } e. _V -> ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0* )
23 xnn0xr 
 |-  ( ( # ` { x e. A | U e. ( I ` x ) } ) e. NN0* -> ( # ` { x e. A | U e. ( I ` x ) } ) e. RR* )
24 21 22 23 mp2b 
 |-  ( # ` { x e. A | U e. ( I ` x ) } ) e. RR*
25 xaddid1 
 |-  ( ( # ` { x e. A | U e. ( I ` x ) } ) e. RR* -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e 0 ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
26 24 25 mp1i 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( ( # ` { x e. A | U e. ( I ` x ) } ) +e 0 ) = ( # ` { x e. A | U e. ( I ` x ) } ) )
27 8 15 26 3eqtrd 
 |-  ( ( I : A --> { x e. ~P V | 2 <_ ( # ` x ) } /\ U e. V ) -> ( D ` U ) = ( # ` { x e. A | U e. ( I ` x ) } ) )