Metamath Proof Explorer

Theorem vtxdeqd

Description: Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021)

Ref Expression
Hypotheses vtxdeqd.g 
|- ( ph -> G e. X )
vtxdeqd.h 
|- ( ph -> H e. Y )
vtxdeqd.v 
|- ( ph -> ( Vtx ` H ) = ( Vtx ` G ) )
vtxdeqd.i 
|- ( ph -> ( iEdg ` H ) = ( iEdg ` G ) )
Assertion vtxdeqd 
|- ( ph -> ( VtxDeg ` H ) = ( VtxDeg ` G ) )

Proof

Step Hyp Ref Expression
1 vtxdeqd.g 
 |-  ( ph -> G e. X )
2 vtxdeqd.h 
 |-  ( ph -> H e. Y )
3 vtxdeqd.v 
 |-  ( ph -> ( Vtx ` H ) = ( Vtx ` G ) )
4 vtxdeqd.i 
 |-  ( ph -> ( iEdg ` H ) = ( iEdg ` G ) )
5 4 dmeqd 
 |-  ( ph -> dom ( iEdg ` H ) = dom ( iEdg ` G ) )
6 4 fveq1d 
 |-  ( ph -> ( ( iEdg ` H ) ` x ) = ( ( iEdg ` G ) ` x ) )
7 6 eleq2d 
 |-  ( ph -> ( u e. ( ( iEdg ` H ) ` x ) <-> u e. ( ( iEdg ` G ) ` x ) ) )
8 5 7 rabeqbidv 
 |-  ( ph -> { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } = { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } )
9 8 fveq2d 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) = ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) )
10 6 eqeq1d 
 |-  ( ph -> ( ( ( iEdg ` H ) ` x ) = { u } <-> ( ( iEdg ` G ) ` x ) = { u } ) )
11 5 10 rabeqbidv 
 |-  ( ph -> { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } = { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } )
12 11 fveq2d 
 |-  ( ph -> ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) = ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) )
13 9 12 oveq12d 
 |-  ( ph -> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) = ( ( # ` { x e. dom ( iEdg ` G ) | u e. ( ( iEdg ` G ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` G ) | ( ( iEdg ` G ) ` x ) = { u } } ) ) )
14 3 13 mpteq12dv 
 |-  ( ph -> ( u e. ( Vtx ` H ) |-> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` 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 } } ) ) ) )
15 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
16 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
17 eqid 
 |-  dom ( iEdg ` H ) = dom ( iEdg ` H )
18 15 16 17 vtxdgfval 
 |-  ( H e. Y -> ( VtxDeg ` H ) = ( u e. ( Vtx ` H ) |-> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) ) )
19 2 18 syl 
 |-  ( ph -> ( VtxDeg ` H ) = ( u e. ( Vtx ` H ) |-> ( ( # ` { x e. dom ( iEdg ` H ) | u e. ( ( iEdg ` H ) ` x ) } ) +e ( # ` { x e. dom ( iEdg ` H ) | ( ( iEdg ` H ) ` x ) = { u } } ) ) ) )
20 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
21 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
22 eqid 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` G )
23 20 21 22 vtxdgfval 
 |-  ( G e. X -> ( 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 } } ) ) ) )
24 1 23 syl 
 |-  ( ph -> ( 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 } } ) ) ) )
25 14 19 24 3eqtr4d 
 |-  ( ph -> ( VtxDeg ` H ) = ( VtxDeg ` G ) )