Theorem p1evtxdp1

Description: If an edge E (not being a loop) which contains vertex U is added to a graph G (yielding a graph F ), the degree of U is increased by 1. (Contributed by AV, 3-Mar-2021)

	Ref	Expression
Hypotheses	p1evtxdeq.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	p1evtxdeq.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	p1evtxdeq.f	⊢ ( 𝜑 → Fun 𝐼 )
	p1evtxdeq.fv	⊢ ( 𝜑 → ( Vtx ‘ 𝐹 ) = 𝑉 )
	p1evtxdeq.fi	⊢ ( 𝜑 → ( iEdg ‘ 𝐹 ) = ( 𝐼 ∪ { ⟨ 𝐾 , 𝐸 ⟩ } ) )
	p1evtxdeq.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
	p1evtxdeq.d	⊢ ( 𝜑 → 𝐾 ∉ dom 𝐼 )
	p1evtxdeq.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	p1evtxdp1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
	p1evtxdp1.n	⊢ ( 𝜑 → 𝑈 ∈ 𝐸 )
	p1evtxdp1.l	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
Assertion	p1evtxdp1	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 ) )

Proof

Step	Hyp	Ref	Expression
1		p1evtxdeq.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		p1evtxdeq.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		p1evtxdeq.f	⊢ ( 𝜑 → Fun 𝐼 )
4		p1evtxdeq.fv	⊢ ( 𝜑 → ( Vtx ‘ 𝐹 ) = 𝑉 )
5		p1evtxdeq.fi	⊢ ( 𝜑 → ( iEdg ‘ 𝐹 ) = ( 𝐼 ∪ { ⟨ 𝐾 , 𝐸 ⟩ } ) )
6		p1evtxdeq.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
7		p1evtxdeq.d	⊢ ( 𝜑 → 𝐾 ∉ dom 𝐼 )
8		p1evtxdeq.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
9		p1evtxdp1.e	⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑉 )
10		p1evtxdp1.n	⊢ ( 𝜑 → 𝑈 ∈ 𝐸 )
11		p1evtxdp1.l	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝐸 ) )
12	1 2 3 4 5 6 7 8 9	p1evtxdeqlem	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) )
13	1	fvexi	⊢ 𝑉 ∈ V
14		snex	⊢ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V
15	13 14	pm3.2i	⊢ ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V )
16		opiedgfv	⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = { ⟨ 𝐾 , 𝐸 ⟩ } )
17	15 16	mp1i	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = { ⟨ 𝐾 , 𝐸 ⟩ } )
18		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = 𝑉 )
19	15 18	mp1i	⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = 𝑉 )
20	17 19 6 8 9 10 11	1hevtxdg1	⊢ ( 𝜑 → ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) = 1 )
21	20	oveq2d	⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 ) )
22	12 21	eqtrd	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +𝑒 1 ) )