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