Metamath Proof Explorer

Theorem vtxdgop

Description: The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021)

Ref Expression
Assertion vtxdgop 
|- ( G e. W -> ( VtxDeg ` G ) = ( ( Vtx ` G ) VtxDeg ( iEdg ` G ) ) )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. ( Vtx ` G ) , ( iEdg ` G ) >. e. _V
2 fvex 
 |-  ( Vtx ` G ) e. _V
3 fvex 
 |-  ( iEdg ` G ) e. _V
4 2 3 opvtxfvi 
 |-  ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( Vtx ` G )
5 4 eqcomi 
 |-  ( Vtx ` G ) = ( Vtx ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
6 2 3 opiedgfvi 
 |-  ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( iEdg ` G )
7 6 eqcomi 
 |-  ( iEdg ` G ) = ( iEdg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
8 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
9 5 7 8 vtxdgfval 
 |-  ( <. ( Vtx ` G ) , ( iEdg ` G ) >. e. _V -> ( VtxDeg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( u e. ( Vtx ` G ) |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) )
10 1 9 mp1i 
 |-  ( G e. W -> ( VtxDeg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) = ( u e. ( Vtx ` G ) |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) )
11 df-ov 
 |-  ( ( Vtx ` G ) VtxDeg ( iEdg ` G ) ) = ( VtxDeg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. )
12 11 a1i 
 |-  ( G e. W -> ( ( Vtx ` G ) VtxDeg ( iEdg ` G ) ) = ( VtxDeg ` <. ( Vtx ` G ) , ( iEdg ` G ) >. ) )
13 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
14 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
15 13 14 8 vtxdgfval 
 |-  ( G e. W -> ( VtxDeg ` G ) = ( u e. ( Vtx ` G ) |-> ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) ) )
16 10 12 15 3eqtr4rd 
 |-  ( G e. W -> ( VtxDeg ` G ) = ( ( Vtx ` G ) VtxDeg ( iEdg ` G ) ) )