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

Metamath Proof Explorer

Theorem vtxdushgrfvedg

Description: The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020) (Proof shortened by AV, 5-May-2021)

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

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v 
 |-  V = ( Vtx ` G )
2 vtxdushgrfvedg.e 
 |-  E = ( Edg ` G )
3 vtxdushgrfvedg.d 
 |-  D = ( VtxDeg ` G )
4 3 fveq1i 
 |-  ( D ` U ) = ( ( VtxDeg ` G ) ` U )
5 4 a1i 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( D ` U ) = ( ( VtxDeg ` G ) ` U ) )
6 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
7 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
8 1 6 7 vtxdgval 
 |-  ( U e. V -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) ) )
9 8 adantl 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) ) )
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 fvex 
 |-  ( iEdg ` G ) e. _V
12 11 dmex 
 |-  dom ( iEdg ` G ) e. _V
13 12 rabex 
 |-  { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } e. _V
14 13 a1i 
 |-  ( ( G e. USHGraph /\ U e. V ) -> { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } e. _V )
15 eqid 
 |-  { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } = { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } }
16 eqeq1 
 |-  ( e = c -> ( e = { U } <-> c = { U } ) )
17 16 cbvrabv 
 |-  { e e. E | e = { U } } = { c e. E | c = { U } }
18 eqid 
 |-  ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } |-> ( ( iEdg ` G ) ` x ) ) = ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } |-> ( ( iEdg ` G ) ` x ) )
19 2 6 15 17 18 ushgredgedgloop 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( x e. { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } |-> ( ( iEdg ` G ) ` x ) ) : { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } -1-1-onto-> { e e. E | e = { U } } )
20 14 19 hasheqf1od 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) = ( # ` { e e. E | e = { U } } ) )
21 10 20 oveq12d 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` i ) = { U } } ) ) = ( ( # ` { e e. E | U e. e } ) +e ( # ` { e e. E | e = { U } } ) ) )
22 5 9 21 3eqtrd 
 |-  ( ( G e. USHGraph /\ U e. V ) -> ( D ` U ) = ( ( # ` { e e. E | U e. e } ) +e ( # ` { e e. E | e = { U } } ) ) )