Metamath Proof Explorer

Theorem vtxdgfval

Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 9-Dec-2020)

Ref Expression
Hypotheses vtxdgfval.v 
|- V = ( Vtx ` G )
vtxdgfval.i 
|- I = ( iEdg ` G )
vtxdgfval.a 
|- A = dom I
Assertion vtxdgfval 
|- ( G e. W -> ( VtxDeg ` G ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )

Proof

Step Hyp Ref Expression
1 vtxdgfval.v 
 |-  V = ( Vtx ` G )
2 vtxdgfval.i 
 |-  I = ( iEdg ` G )
3 vtxdgfval.a 
 |-  A = dom I
4 df-vtxdg 
 |-  VtxDeg = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
5 fvex 
 |-  ( Vtx ` g ) e. _V
6 fvex 
 |-  ( iEdg ` g ) e. _V
7 simpl 
 |-  ( ( v = ( Vtx ` g ) /\ e = ( iEdg ` g ) ) -> v = ( Vtx ` g ) )
8 dmeq 
 |-  ( e = ( iEdg ` g ) -> dom e = dom ( iEdg ` g ) )
9 fveq1 
 |-  ( e = ( iEdg ` g ) -> ( e ` x ) = ( ( iEdg ` g ) ` x ) )
10 9 eleq2d 
 |-  ( e = ( iEdg ` g ) -> ( u e. ( e ` x ) <-> u e. ( ( iEdg ` g ) ` x ) ) )
11 8 10 rabeqbidv 
 |-  ( e = ( iEdg ` g ) -> { x e. dom e | u e. ( e ` x ) } = { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } )
12 11 fveq2d 
 |-  ( e = ( iEdg ` g ) -> ( # ` { x e. dom e | u e. ( e ` x ) } ) = ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) )
13 9 eqeq1d 
 |-  ( e = ( iEdg ` g ) -> ( ( e ` x ) = { u } <-> ( ( iEdg ` g ) ` x ) = { u } ) )
14 8 13 rabeqbidv 
 |-  ( e = ( iEdg ` g ) -> { x e. dom e | ( e ` x ) = { u } } = { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } )
15 14 fveq2d 
 |-  ( e = ( iEdg ` g ) -> ( # ` { x e. dom e | ( e ` x ) = { u } } ) = ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) )
16 12 15 oveq12d 
 |-  ( e = ( iEdg ` g ) -> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) = ( ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) ) )
17 16 adantl 
 |-  ( ( v = ( Vtx ` g ) /\ e = ( iEdg ` g ) ) -> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) = ( ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) ) )
18 7 17 mpteq12dv 
 |-  ( ( v = ( Vtx ` g ) /\ e = ( iEdg ` g ) ) -> ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) = ( u e. ( Vtx ` g ) |-> ( ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) ) ) )
19 5 6 18 csbie2 
 |-  [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) = ( u e. ( Vtx ` g ) |-> ( ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) ) )
20 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
21 20 1 eqtr4di 
 |-  ( g = G -> ( Vtx ` g ) = V )
22 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
23 22 dmeqd 
 |-  ( g = G -> dom ( iEdg ` g ) = dom ( iEdg ` G ) )
24 2 dmeqi 
 |-  dom I = dom ( iEdg ` G )
25 3 24 eqtri 
 |-  A = dom ( iEdg ` G )
26 23 25 eqtr4di 
 |-  ( g = G -> dom ( iEdg ` g ) = A )
27 22 2 eqtr4di 
 |-  ( g = G -> ( iEdg ` g ) = I )
28 27 fveq1d 
 |-  ( g = G -> ( ( iEdg ` g ) ` x ) = ( I ` x ) )
29 28 eleq2d 
 |-  ( g = G -> ( u e. ( ( iEdg ` g ) ` x ) <-> u e. ( I ` x ) ) )
30 26 29 rabeqbidv 
 |-  ( g = G -> { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } = { x e. A | u e. ( I ` x ) } )
31 30 fveq2d 
 |-  ( g = G -> ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) = ( # ` { x e. A | u e. ( I ` x ) } ) )
32 28 eqeq1d 
 |-  ( g = G -> ( ( ( iEdg ` g ) ` x ) = { u } <-> ( I ` x ) = { u } ) )
33 26 32 rabeqbidv 
 |-  ( g = G -> { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } = { x e. A | ( I ` x ) = { u } } )
34 33 fveq2d 
 |-  ( g = G -> ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) = ( # ` { x e. A | ( I ` x ) = { u } } ) )
35 31 34 oveq12d 
 |-  ( g = G -> ( ( # ` { x e. dom ( iEdg ` g ) | u e. ( ( iEdg ` g ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` g ) | ( ( iEdg ` g ) ` x ) = { u } } ) ) = ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) )
36 21 35 mpteq12dv 
 |-  ( g = 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 } } ) ) ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )
37 36 adantl 
 |-  ( ( G e. W /\ g = 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 } } ) ) ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )
38 19 37 syl5eq 
 |-  ( ( G e. W /\ g = G ) -> [_ ( Vtx ` g ) / v ]_ [_ ( iEdg ` g ) / e ]_ ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )
39 elex 
 |-  ( G e. W -> G e. _V )
40 1 fvexi 
 |-  V e. _V
41 mptexg 
 |-  ( V e. _V -> ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) e. _V )
42 40 41 mp1i 
 |-  ( G e. W -> ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) e. _V )
43 4 38 39 42 fvmptd2 
 |-  ( G e. W -> ( VtxDeg ` G ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( I ` x ) } ) +e ( # ` { x e. A | ( I ` x ) = { u } } ) ) ) )