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 ( 𝜑𝐺𝑋 )
vtxdeqd.h ( 𝜑𝐻𝑌 )
vtxdeqd.v ( 𝜑 → ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐺 ) )
vtxdeqd.i ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 ) )
Assertion vtxdeqd ( 𝜑 → ( VtxDeg ‘ 𝐻 ) = ( VtxDeg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 vtxdeqd.g ( 𝜑𝐺𝑋 )
2 vtxdeqd.h ( 𝜑𝐻𝑌 )
3 vtxdeqd.v ( 𝜑 → ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐺 ) )
4 vtxdeqd.i ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 ) )
5 4 dmeqd ( 𝜑 → dom ( iEdg ‘ 𝐻 ) = dom ( iEdg ‘ 𝐺 ) )
6 4 fveq1d ( 𝜑 → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
7 6 eleq2d ( 𝜑 → ( 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ↔ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
8 5 7 rabeqbidv ( 𝜑 → { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } )
9 8 fveq2d ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) } ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
10 6 eqeq1d ( 𝜑 → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } ) )
11 5 10 rabeqbidv ( 𝜑 → { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } )
12 11 fveq2d ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } } ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) )
13 9 12 oveq12d ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } } ) ) = ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) )
14 3 13 mpteq12dv ( 𝜑 → ( 𝑢 ∈ ( Vtx ‘ 𝐻 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) = ( 𝑢 ∈ ( Vtx ‘ 𝐺 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
15 eqid ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
16 eqid ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
17 eqid dom ( iEdg ‘ 𝐻 ) = dom ( iEdg ‘ 𝐻 )
18 15 16 17 vtxdgfval ( 𝐻𝑌 → ( VtxDeg ‘ 𝐻 ) = ( 𝑢 ∈ ( Vtx ‘ 𝐻 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
19 2 18 syl ( 𝜑 → ( VtxDeg ‘ 𝐻 ) = ( 𝑢 ∈ ( Vtx ‘ 𝐻 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
20 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
21 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
22 eqid dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
23 20 21 22 vtxdgfval ( 𝐺𝑋 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢 ∈ ( Vtx ‘ 𝐺 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
24 1 23 syl ( 𝜑 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢 ∈ ( Vtx ‘ 𝐺 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
25 14 19 24 3eqtr4d ( 𝜑 → ( VtxDeg ‘ 𝐻 ) = ( VtxDeg ‘ 𝐺 ) )