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	$⊢ V = Vtx (G)$
	p1evtxdeq.i	$⊢ I = iEdg (G)$
	p1evtxdeq.f	$⊢ φ \to Fun I$
	p1evtxdeq.fv	$⊢ φ \to Vtx (F) = V$
	p1evtxdeq.fi	$⊢ φ \to iEdg (F) = I \cup \{⟨K, E⟩\}$
	p1evtxdeq.k	$⊢ φ \to K \in X$
	p1evtxdeq.d	$⊢ φ \to K \notin dom I$
	p1evtxdeq.u	$⊢ φ \to U \in V$
	p1evtxdeq.e	$⊢ φ \to E \in Y$
	p1evtxdeq.n	$⊢ φ \to U \notin E$
Assertion	p1evtxdeq	$⊢ φ \to VtxDeg (F) (U) = VtxDeg (G) (U)$

Proof

Step	Hyp	Ref	Expression
1		p1evtxdeq.v	$⊢ V = Vtx (G)$
2		p1evtxdeq.i	$⊢ I = iEdg (G)$
3		p1evtxdeq.f	$⊢ φ \to Fun I$
4		p1evtxdeq.fv	$⊢ φ \to Vtx (F) = V$
5		p1evtxdeq.fi	$⊢ φ \to iEdg (F) = I \cup \{⟨K, E⟩\}$
6		p1evtxdeq.k	$⊢ φ \to K \in X$
7		p1evtxdeq.d	$⊢ φ \to K \notin dom I$
8		p1evtxdeq.u	$⊢ φ \to U \in V$
9		p1evtxdeq.e	$⊢ φ \to E \in Y$
10		p1evtxdeq.n	$⊢ φ \to U \notin E$
11	1 2 3 4 5 6 7 8 9	p1evtxdeqlem	$⊢ φ \to VtxDeg (F) (U) = VtxDeg (G) (U) +_{𝑒} VtxDeg (⟨V, \{⟨K, E⟩\}⟩) (U)$
12	1	fvexi	$⊢ V \in V$
13		snex	$⊢ \{⟨K, E⟩\} \in V$
14	12 13	pm3.2i	$⊢ (V \in V \land \{⟨K, E⟩\} \in V)$
15		opiedgfv	$⊢ (V \in V \land \{⟨K, E⟩\} \in V) \to iEdg (⟨V, \{⟨K, E⟩\}⟩) = \{⟨K, E⟩\}$
16	14 15	mp1i	$⊢ φ \to iEdg (⟨V, \{⟨K, E⟩\}⟩) = \{⟨K, E⟩\}$
17		opvtxfv	$⊢ (V \in V \land \{⟨K, E⟩\} \in V) \to Vtx (⟨V, \{⟨K, E⟩\}⟩) = V$
18	14 17	mp1i	$⊢ φ \to Vtx (⟨V, \{⟨K, E⟩\}⟩) = V$
19	16 18 6 8 9 10	1hevtxdg0	$⊢ φ \to VtxDeg (⟨V, \{⟨K, E⟩\}⟩) (U) = 0$
20	19	oveq2d	$⊢ φ \to VtxDeg (G) (U) +_{𝑒} VtxDeg (⟨V, \{⟨K, E⟩\}⟩) (U) = VtxDeg (G) (U) +_{𝑒} 0$
21	1	vtxdgelxnn0	$⊢ U \in V \to VtxDeg (G) (U) \in ℕ_{0}^{*}$
22		xnn0xr	$⊢ VtxDeg (G) (U) \in ℕ_{0}^{} \to VtxDeg (G) (U) \in ℝ^{}$
23	8 21 22	3syl	$⊢ φ \to VtxDeg (G) (U) \in ℝ^{*}$
24	23	xaddid1d	$⊢ φ \to VtxDeg (G) (U) +_{𝑒} 0 = VtxDeg (G) (U)$
25	11 20 24	3eqtrd	$⊢ φ \to VtxDeg (F) (U) = VtxDeg (G) (U)$

Metamath Proof Explorer

Theorem p1evtxdeq

Proof