Step | Hyp | Ref
| Expression |
1 | | vtxdeqd.v |
. . 3
⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺)) |
2 | | vtxdeqd.i |
. . . . . . 7
⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺)) |
3 | 2 | dmeqd 5326 |
. . . . . 6
⊢ (𝜑 → dom (iEdg‘𝐻) = dom (iEdg‘𝐺)) |
4 | 2 | fveq1d 6193 |
. . . . . . 7
⊢ (𝜑 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐺)‘𝑥)) |
5 | 4 | eleq2d 2687 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ ((iEdg‘𝐻)‘𝑥) ↔ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥))) |
6 | 3, 5 | rabeqbidv 3195 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) |
7 | 6 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) = (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)})) |
8 | 4 | eqeq1d 2624 |
. . . . . 6
⊢ (𝜑 → (((iEdg‘𝐻)‘𝑥) = {𝑢} ↔ ((iEdg‘𝐺)‘𝑥) = {𝑢})) |
9 | 3, 8 | rabeqbidv 3195 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}}) |
10 | 9 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}}) = (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}})) |
11 | 7, 10 | oveq12d 6668 |
. . 3
⊢ (𝜑 → ((#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}}))) |
12 | 1, 11 | mpteq12dv 4733 |
. 2
⊢ (𝜑 → (𝑢 ∈ (Vtx‘𝐻) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}})))) |
13 | | vtxdeqd.h |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑌) |
14 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
15 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) |
16 | | eqid 2622 |
. . . 4
⊢ dom
(iEdg‘𝐻) = dom
(iEdg‘𝐻) |
17 | 14, 15, 16 | vtxdgfval 26363 |
. . 3
⊢ (𝐻 ∈ 𝑌 → (VtxDeg‘𝐻) = (𝑢 ∈ (Vtx‘𝐻) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}})))) |
18 | 13, 17 | syl 17 |
. 2
⊢ (𝜑 → (VtxDeg‘𝐻) = (𝑢 ∈ (Vtx‘𝐻) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}})))) |
19 | | vtxdeqd.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑋) |
20 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
21 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
22 | | eqid 2622 |
. . . 4
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
23 | 20, 21, 22 | vtxdgfval 26363 |
. . 3
⊢ (𝐺 ∈ 𝑋 → (VtxDeg‘𝐺) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}})))) |
24 | 19, 23 | syl 17 |
. 2
⊢ (𝜑 → (VtxDeg‘𝐺) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}})))) |
25 | 12, 18, 24 | 3eqtr4d 2666 |
1
⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺)) |