Metamath Proof Explorer

Theorem vtxdg0e

Description: The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai , vdegp1bi and vdegp1ci ). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypotheses vtxdgf.v 
|- V = ( Vtx ` G )
vtxdg0e.i 
|- I = ( iEdg ` G )
Assertion vtxdg0e 
|- ( ( U e. V /\ I = (/) ) -> ( ( VtxDeg ` G ) ` U ) = 0 )

Proof

Step Hyp Ref Expression
1 vtxdgf.v 
 |-  V = ( Vtx ` G )
2 vtxdg0e.i 
 |-  I = ( iEdg ` G )
3 2 eqeq1i 
 |-  ( I = (/) <-> ( iEdg ` G ) = (/) )
4 dmeq 
 |-  ( ( iEdg ` G ) = (/) -> dom ( iEdg ` G ) = dom (/) )
5 dm0 
 |-  dom (/) = (/)
6 4 5 eqtrdi 
 |-  ( ( iEdg ` G ) = (/) -> dom ( iEdg ` G ) = (/) )
7 0fin 
 |-  (/) e. Fin
8 6 7 eqeltrdi 
 |-  ( ( iEdg ` G ) = (/) -> dom ( iEdg ` G ) e. Fin )
9 3 8 sylbi 
 |-  ( I = (/) -> dom ( iEdg ` G ) e. Fin )
10 simpl 
 |-  ( ( U e. V /\ I = (/) ) -> U e. V )
11 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
12 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
13 1 11 12 vtxdgfival 
 |-  ( ( dom ( iEdg ` G ) e. Fin /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) + ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) ) )
14 9 10 13 syl2an2 
 |-  ( ( U e. V /\ I = (/) ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) + ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) ) )
15 3 6 sylbi 
 |-  ( I = (/) -> dom ( iEdg ` G ) = (/) )
16 15 adantl 
 |-  ( ( U e. V /\ I = (/) ) -> dom ( iEdg ` G ) = (/) )
17 rabeq 
 |-  ( dom ( iEdg ` G ) = (/) -> { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } = { x e. (/) | U e. ( ( iEdg ` G ) ` x ) } )
18 rab0 
 |-  { x e. (/) | U e. ( ( iEdg ` G ) ` x ) } = (/)
19 17 18 eqtrdi 
 |-  ( dom ( iEdg ` G ) = (/) -> { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } = (/) )
20 19 fveq2d 
 |-  ( dom ( iEdg ` G ) = (/) -> ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) = ( # ` (/) ) )
21 hash0 
 |-  ( # ` (/) ) = 0
22 20 21 eqtrdi 
 |-  ( dom ( iEdg ` G ) = (/) -> ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) = 0 )
23 rabeq 
 |-  ( dom ( iEdg ` G ) = (/) -> { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } = { x e. (/) | ( ( iEdg ` G ) ` x ) = { U } } )
24 23 fveq2d 
 |-  ( dom ( iEdg ` G ) = (/) -> ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) = ( # ` { x e. (/) | ( ( iEdg ` G ) ` x ) = { U } } ) )
25 rab0 
 |-  { x e. (/) | ( ( iEdg ` G ) ` x ) = { U } } = (/)
26 25 fveq2i 
 |-  ( # ` { x e. (/) | ( ( iEdg ` G ) ` x ) = { U } } ) = ( # ` (/) )
27 26 21 eqtri 
 |-  ( # ` { x e. (/) | ( ( iEdg ` G ) ` x ) = { U } } ) = 0
28 24 27 eqtrdi 
 |-  ( dom ( iEdg ` G ) = (/) -> ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) = 0 )
29 22 28 oveq12d 
 |-  ( dom ( iEdg ` G ) = (/) -> ( ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) + ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) ) = ( 0 + 0 ) )
30 16 29 syl 
 |-  ( ( U e. V /\ I = (/) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) + ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) ) = ( 0 + 0 ) )
31 00id 
 |-  ( 0 + 0 ) = 0
32 30 31 eqtrdi 
 |-  ( ( U e. V /\ I = (/) ) -> ( ( # ` { x e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` x ) } ) + ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { U } } ) ) = 0 )
33 14 32 eqtrd 
 |-  ( ( U e. V /\ I = (/) ) -> ( ( VtxDeg ` G ) ` U ) = 0 )