p1evtxdeq

Description: If an edge E which does not contain vertex U is added to a graph G (yielding a graph F ), the degree of U is the same in both graphs. (Contributed by AV, 2-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	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	p1evtxdeq.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
	p1evtxdeq.n	⊢ ( 𝜑 → 𝑈 ∉ 𝐸 )
Assertion	p1evtxdeq	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )

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		p1evtxdeq.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
10		p1evtxdeq.n	⊢ ( 𝜑 → 𝑈 ∉ 𝐸 )
11	1 2 3 4 5 6 7 8 9	p1evtxdeqlem	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +_𝑒 ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) )
12	1	fvexi	⊢ 𝑉 ∈ V
13		snex	⊢ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V
14	12 13	pm3.2i	⊢ ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V )
15		opiedgfv	⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = { ⟨ 𝐾 , 𝐸 ⟩ } )
16	14 15	mp1i	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = { ⟨ 𝐾 , 𝐸 ⟩ } )
17		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ { ⟨ 𝐾 , 𝐸 ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = 𝑉 )
18	14 17	mp1i	⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) = 𝑉 )
19	16 18 6 8 9 10	1hevtxdg0	⊢ ( 𝜑 → ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) = 0 )
20	19	oveq2d	⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +_𝑒 ( ( VtxDeg ‘ ⟨ 𝑉 , { ⟨ 𝐾 , 𝐸 ⟩ } ⟩ ) ‘ 𝑈 ) ) = ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +_𝑒 0 ) )
21	1	vtxdgelxnn0	⊢ ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℕ₀^* )
22		xnn0xr	⊢ ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℕ₀^* → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℝ^* )
23	8 21 22	3syl	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ∈ ℝ^* )
24	23	xaddridd	⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) +_𝑒 0 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )
25	11 20 24	3eqtrd	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐹 ) ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )

Metamath Proof Explorer

Theorem p1evtxdeq

Proof