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 ) )