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