This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtxdgop

Description: The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021)

Ref Expression
Assertion vtxdgop ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) = ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ V
2 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
3 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
4 2 3 opvtxfvi ⊢ ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( Vtx ‘ 𝐺 )
5 4 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ )
6 2 3 opiedgfvi ⊢ ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( iEdg ‘ 𝐺 )
7 6 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ )
8 eqid ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
9 5 7 8 vtxdgfval ⊢ ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ V → ( VtxDeg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( 𝑢 ∈ ( Vtx ‘ 𝐺 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
10 1 9 mp1i ⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) = ( 𝑢 ∈ ( Vtx ‘ 𝐺 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
11 df-ov ⊢ ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) = ( VtxDeg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ )
12 11 a1i ⊢ ( 𝐺 ∈ 𝑊 → ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) = ( VtxDeg ‘ ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ) )
13 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
14 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
15 13 14 8 vtxdgfval ⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) = ( 𝑢 ∈ ( Vtx ‘ 𝐺 ) ↦ ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑢 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) +𝑒 ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = { 𝑢 } } ) ) ) )
16 10 12 15 3eqtr4rd ⊢ ( 𝐺 ∈ 𝑊 → ( VtxDeg ‘ 𝐺 ) = ( ( Vtx ‘ 𝐺 ) VtxDeg ( iEdg ‘ 𝐺 ) ) )