Theorem vtxdgfval 26363

Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.)

Hypotheses

Ref	Expression
vtxdgfval.v	⊢ 𝑉 = (Vtx‘𝐺)
vtxdgfval.i	⊢ 𝐼 = (iEdg‘𝐺)
vtxdgfval.a	⊢ 𝐴 = dom 𝐼

Assertion

Ref	Expression
vtxdgfval	⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))

Distinct variable groups:   𝑥,𝑢   𝑥,𝐴   𝑢,𝐺,𝑥   𝑢,𝑉

Allowed substitution hints:   𝐴(𝑢)   𝐼(𝑥,𝑢)   𝑉(𝑥)   𝑊(𝑥,𝑢)

Proof of Theorem vtxdgfval

Dummy variables 𝑒 𝑔 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-vtxdg 26362	. . 3 ⊢ VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))
2	1	a1i 11	. 2 ⊢ (𝐺 ∈ 𝑊 → VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))))
3		fvex 6201	. . . 4 ⊢ (Vtx‘𝑔) ∈ V
4		fvex 6201	. . . 4 ⊢ (iEdg‘𝑔) ∈ V
5		simpl 473	. . . . 5 ⊢ ((𝑣 = (Vtx‘𝑔) ∧ 𝑒 = (iEdg‘𝑔)) → 𝑣 = (Vtx‘𝑔))
6		dmeq 5324	. . . . . . . . 9 ⊢ (𝑒 = (iEdg‘𝑔) → dom 𝑒 = dom (iEdg‘𝑔))
7		fveq1 6190	. . . . . . . . . 10 ⊢ (𝑒 = (iEdg‘𝑔) → (𝑒‘𝑥) = ((iEdg‘𝑔)‘𝑥))
8	7	eleq2d 2687	. . . . . . . . 9 ⊢ (𝑒 = (iEdg‘𝑔) → (𝑢 ∈ (𝑒‘𝑥) ↔ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)))
9	6, 8	rabeqbidv 3195	. . . . . . . 8 ⊢ (𝑒 = (iEdg‘𝑔) → {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)} = {𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)})
10	9	fveq2d 6195	. . . . . . 7 ⊢ (𝑒 = (iEdg‘𝑔) → (#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) = (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}))
11	7	eqeq1d 2624	. . . . . . . . 9 ⊢ (𝑒 = (iEdg‘𝑔) → ((𝑒‘𝑥) = {𝑢} ↔ ((iEdg‘𝑔)‘𝑥) = {𝑢}))
12	6, 11	rabeqbidv 3195	. . . . . . . 8 ⊢ (𝑒 = (iEdg‘𝑔) → {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}} = {𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})
13	12	fveq2d 6195	. . . . . . 7 ⊢ (𝑒 = (iEdg‘𝑔) → (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}) = (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))
14	10, 13	oveq12d 6668	. . . . . 6 ⊢ (𝑒 = (iEdg‘𝑔) → ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})))
15	14	adantl 482	. . . . 5 ⊢ ((𝑣 = (Vtx‘𝑔) ∧ 𝑒 = (iEdg‘𝑔)) → ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})))
16	5, 15	mpteq12dv 4733	. . . 4 ⊢ ((𝑣 = (Vtx‘𝑔) ∧ 𝑒 = (iEdg‘𝑔)) → (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))))
17	3, 4, 16	csbie2 3563	. . 3 ⊢ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})))
18		fveq2 6191	. . . . . 6 ⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺))
19		vtxdgfval.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
20	18, 19	syl6eqr 2674	. . . . 5 ⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = 𝑉)
21		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = (iEdg‘𝐺))
22	21	dmeqd 5326	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = dom (iEdg‘𝐺))
23		vtxdgfval.a	. . . . . . . . . 10 ⊢ 𝐴 = dom 𝐼
24		vtxdgfval.i	. . . . . . . . . . 11 ⊢ 𝐼 = (iEdg‘𝐺)
25	24	dmeqi 5325	. . . . . . . . . 10 ⊢ dom 𝐼 = dom (iEdg‘𝐺)
26	23, 25	eqtri 2644	. . . . . . . . 9 ⊢ 𝐴 = dom (iEdg‘𝐺)
27	22, 26	syl6eqr 2674	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → dom (iEdg‘𝑔) = 𝐴)
28	21, 24	syl6eqr 2674	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (iEdg‘𝑔) = 𝐼)
29	28	fveq1d 6193	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((iEdg‘𝑔)‘𝑥) = (𝐼‘𝑥))
30	29	eleq2d 2687	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝑢 ∈ ((iEdg‘𝑔)‘𝑥) ↔ 𝑢 ∈ (𝐼‘𝑥)))
31	27, 30	rabeqbidv 3195	. . . . . . 7 ⊢ (𝑔 = 𝐺 → {𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)})
32	31	fveq2d 6195	. . . . . 6 ⊢ (𝑔 = 𝐺 → (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) = (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}))
33	29	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (((iEdg‘𝑔)‘𝑥) = {𝑢} ↔ (𝐼‘𝑥) = {𝑢}))
34	27, 33	rabeqbidv 3195	. . . . . . 7 ⊢ (𝑔 = 𝐺 → {𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}} = {𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})
35	34	fveq2d 6195	. . . . . 6 ⊢ (𝑔 = 𝐺 → (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}) = (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))
36	32, 35	oveq12d 6668	. . . . 5 ⊢ (𝑔 = 𝐺 → ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))
37	20, 36	mpteq12dv 4733	. . . 4 ⊢ (𝑔 = 𝐺 → (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))
38	37	adantl 482	. . 3 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺) → (𝑢 ∈ (Vtx‘𝑔) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ 𝑢 ∈ ((iEdg‘𝑔)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝑔) ∣ ((iEdg‘𝑔)‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))
39	17, 38	syl5eq 2668	. 2 ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑔 = 𝐺) → ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))
40		elex 3212	. 2 ⊢ (𝐺 ∈ 𝑊 → 𝐺 ∈ V)
41		fvex 6201	. . . 4 ⊢ (Vtx‘𝐺) ∈ V
42	19, 41	eqeltri 2697	. . 3 ⊢ 𝑉 ∈ V
43		mptexg 6484	. . 3 ⊢ (𝑉 ∈ V → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))) ∈ V)
44	42, 43	mp1i 13	. 2 ⊢ (𝐺 ∈ 𝑊 → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))) ∈ V)
45	2, 39, 40, 44	fvmptd 6288	1 ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}}))))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {crab 2916  Vcvv 3200  ⦋csb 3533  {csn 4177   ↦ cmpt 4729  dom cdm 5114  ‘cfv 5888  (class class class)co 6650   +_𝑒 cxad 11944  #chash 13117  Vtxcvtx 25874  iEdgciedg 25875  VtxDegcvtxdg 26361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-vtxdg 26362

This theorem is referenced by:  vtxdgval  26364  vtxdgop  26366  vtxdgf  26367  vtxdeqd  26373