vtxdeqd

Description: Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021)

	Ref	Expression
Hypotheses	vtxdeqd.g	$⊢ φ \to G \in X$
	vtxdeqd.h	$⊢ φ \to H \in Y$
	vtxdeqd.v	$⊢ φ \to Vtx (H) = Vtx (G)$
	vtxdeqd.i	$⊢ φ \to iEdg (H) = iEdg (G)$
Assertion	vtxdeqd	$⊢ φ \to VtxDeg (H) = VtxDeg (G)$

Proof

Step	Hyp	Ref	Expression
1		vtxdeqd.g	$⊢ φ \to G \in X$
2		vtxdeqd.h	$⊢ φ \to H \in Y$
3		vtxdeqd.v	$⊢ φ \to Vtx (H) = Vtx (G)$
4		vtxdeqd.i	$⊢ φ \to iEdg (H) = iEdg (G)$
5	4	dmeqd	$⊢ φ \to dom iEdg (H) = dom iEdg (G)$
6	4	fveq1d	$⊢ φ \to iEdg (H) (x) = iEdg (G) (x)$
7	6	eleq2d	$⊢ φ \to (u \in iEdg (H) (x) \leftrightarrow u \in iEdg (G) (x))$
8	5 7	rabeqbidv	$⊢ φ \to \{x \in dom iEdg (H) \| u \in iEdg (H) (x)\} = \{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}$
9	8	fveq2d	$⊢ φ \to \|\{x \in dom iEdg (H) \| u \in iEdg (H) (x)\}\| = \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\|$
10	6	eqeq1d	$⊢ φ \to (iEdg (H) (x) = \{u\} \leftrightarrow iEdg (G) (x) = \{u\})$
11	5 10	rabeqbidv	$⊢ φ \to \{x \in dom iEdg (H) \| iEdg (H) (x) = \{u\}\} = \{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}$
12	11	fveq2d	$⊢ φ \to \|\{x \in dom iEdg (H) \| iEdg (H) (x) = \{u\}\}\| = \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\|$
13	9 12	oveq12d	$⊢ φ \to \|\{x \in dom iEdg (H) \| u \in iEdg (H) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (H) \| iEdg (H) (x) = \{u\}\}\| = \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\|$
14	3 13	mpteq12dv	$⊢ φ \to (u \in Vtx (H) ⟼ \|\{x \in dom iEdg (H) \| u \in iEdg (H) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (H) \| iEdg (H) (x) = \{u\}\}\|) = (u \in Vtx (G) ⟼ \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\|)$
15		eqid	$⊢ Vtx (H) = Vtx (H)$
16		eqid	$⊢ iEdg (H) = iEdg (H)$
17		eqid	$⊢ dom iEdg (H) = dom iEdg (H)$
18	15 16 17	vtxdgfval	$⊢ H \in Y \to VtxDeg (H) = (u \in Vtx (H) ⟼ \|\{x \in dom iEdg (H) \| u \in iEdg (H) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (H) \| iEdg (H) (x) = \{u\}\}\|)$
19	2 18	syl	$⊢ φ \to VtxDeg (H) = (u \in Vtx (H) ⟼ \|\{x \in dom iEdg (H) \| u \in iEdg (H) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (H) \| iEdg (H) (x) = \{u\}\}\|)$
20		eqid	$⊢ Vtx (G) = Vtx (G)$
21		eqid	$⊢ iEdg (G) = iEdg (G)$
22		eqid	$⊢ dom iEdg (G) = dom iEdg (G)$
23	20 21 22	vtxdgfval	$⊢ G \in X \to VtxDeg (G) = (u \in Vtx (G) ⟼ \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\|)$
24	1 23	syl	$⊢ φ \to VtxDeg (G) = (u \in Vtx (G) ⟼ \|\{x \in dom iEdg (G) \| u \in iEdg (G) (x)\}\| +_{𝑒} \|\{x \in dom iEdg (G) \| iEdg (G) (x) = \{u\}\}\|)$
25	14 19 24	3eqtr4d	$⊢ φ \to VtxDeg (H) = VtxDeg (G)$

Metamath Proof Explorer

Theorem vtxdeqd

Proof