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

Metamath Proof Explorer

Theorem vtxdusgrfvedg

Description: The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v 
|- V = ( Vtx ` G )
vtxdushgrfvedg.e 
|- E = ( Edg ` G )
vtxdushgrfvedg.d 
|- D = ( VtxDeg ` G )
Assertion vtxdusgrfvedg 
|- ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { e e. E | U e. e } ) )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v 
 |-  V = ( Vtx ` G )
2 vtxdushgrfvedg.e 
 |-  E = ( Edg ` G )
3 vtxdushgrfvedg.d 
 |-  D = ( VtxDeg ` G )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
6 1 4 5 3 vtxdusgrval 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) )
7 usgruspgr 
 |-  ( G e. USGraph -> G e. USPGraph )
8 uspgrushgr 
 |-  ( G e. USPGraph -> G e. USHGraph )
9 7 8 syl 
 |-  ( G e. USGraph -> G e. USHGraph )
10 1 2 vtxdushgrfvedglem 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )
11 9 10 sylan 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) )
12 6 11 eqtrd 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( D ` U ) = ( # ` { e e. E | U e. e } ) )