Metamath Proof Explorer

Theorem vtxdgop

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

Ref Expression
Assertion vtxdgop ⊢ G ∈ W → VtxDeg ⁡ G = Vtx ⁡ G VtxDeg iEdg ⁡ G

Proof

Step Hyp Ref Expression
1 opex ⊢ Vtx ⁡ G iEdg ⁡ G ∈ V
2 fvex ⊢ Vtx ⁡ G ∈ V
3 fvex ⊢ iEdg ⁡ G ∈ V
4 2 3 opvtxfvi ⊢ Vtx ⁡ Vtx ⁡ G iEdg ⁡ G = Vtx ⁡ G
5 4 eqcomi ⊢ Vtx ⁡ G = Vtx ⁡ Vtx ⁡ G iEdg ⁡ G
6 2 3 opiedgfvi ⊢ iEdg ⁡ Vtx ⁡ G iEdg ⁡ G = iEdg ⁡ G
7 6 eqcomi ⊢ iEdg ⁡ G = iEdg ⁡ Vtx ⁡ G iEdg ⁡ G
8 eqid ⊢ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
9 5 7 8 vtxdgfval ⊢ Vtx ⁡ G iEdg ⁡ G ∈ V → VtxDeg ⁡ Vtx ⁡ G iEdg ⁡ G = u ∈ Vtx ⁡ G ⟼ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u
10 1 9 mp1i ⊢ G ∈ W → VtxDeg ⁡ Vtx ⁡ G iEdg ⁡ G = u ∈ Vtx ⁡ G ⟼ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u
11 df-ov ⊢ Vtx ⁡ G VtxDeg iEdg ⁡ G = VtxDeg ⁡ Vtx ⁡ G iEdg ⁡ G
12 11 a1i ⊢ G ∈ W → Vtx ⁡ G VtxDeg iEdg ⁡ G = VtxDeg ⁡ Vtx ⁡ G iEdg ⁡ G
13 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
14 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
15 13 14 8 vtxdgfval ⊢ G ∈ W → VtxDeg ⁡ G = u ∈ Vtx ⁡ G ⟼ x ∈ dom ⁡ iEdg ⁡ G | u ∈ iEdg ⁡ G ⁡ x + 𝑒 x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = u
16 10 12 15 3eqtr4rd ⊢ G ∈ W → VtxDeg ⁡ G = Vtx ⁡ G VtxDeg iEdg ⁡ G