Metamath Proof Explorer

Theorem umgrres

Description: A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 ) is a multigraph. (Contributed by AV, 27-Nov-2020) (Revised by AV, 19-Dec-2021)

Ref Expression
Hypotheses upgrres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
upgrres.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
upgrres.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
upgrres.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{E}↾}_{{F}}⟩$
Assertion umgrres ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to {S}\in \mathrm{UMGraph}$

Proof

Step Hyp Ref Expression
1 upgrres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 upgrres.e ${⊢}{E}=\mathrm{iEdg}\left({G}\right)$
3 upgrres.f ${⊢}{F}=\left\{{i}\in \mathrm{dom}{E}|{N}\notin {E}\left({i}\right)\right\}$
4 upgrres.s ${⊢}{S}=⟨{V}\setminus \left\{{N}\right\},{{E}↾}_{{F}}⟩$
5 umgruhgr ${⊢}{G}\in \mathrm{UMGraph}\to {G}\in \mathrm{UHGraph}$
6 2 uhgrfun ${⊢}{G}\in \mathrm{UHGraph}\to \mathrm{Fun}{E}$
7 funres ${⊢}\mathrm{Fun}{E}\to \mathrm{Fun}\left({{E}↾}_{{F}}\right)$
8 5 6 7 3syl ${⊢}{G}\in \mathrm{UMGraph}\to \mathrm{Fun}\left({{E}↾}_{{F}}\right)$
9 8 funfnd ${⊢}{G}\in \mathrm{UMGraph}\to \left({{E}↾}_{{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{{F}}\right)$
10 9 adantr ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \left({{E}↾}_{{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{{F}}\right)$
11 1 2 3 umgrreslem ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
12 df-f ${⊢}\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)⟶\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}↔\left(\left({{E}↾}_{{F}}\right)Fn\mathrm{dom}\left({{E}↾}_{{F}}\right)\wedge \mathrm{ran}\left({{E}↾}_{{F}}\right)\subseteq \left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
13 10 11 12 sylanbrc ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)⟶\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}$
14 opex ${⊢}⟨{V}\setminus \left\{{N}\right\},{{E}↾}_{{F}}⟩\in \mathrm{V}$
15 4 14 eqeltri ${⊢}{S}\in \mathrm{V}$
16 1 2 3 4 uhgrspan1lem2 ${⊢}\mathrm{Vtx}\left({S}\right)={V}\setminus \left\{{N}\right\}$
17 16 eqcomi ${⊢}{V}\setminus \left\{{N}\right\}=\mathrm{Vtx}\left({S}\right)$
18 1 2 3 4 uhgrspan1lem3 ${⊢}\mathrm{iEdg}\left({S}\right)={{E}↾}_{{F}}$
19 18 eqcomi ${⊢}{{E}↾}_{{F}}=\mathrm{iEdg}\left({S}\right)$
20 17 19 isumgrs ${⊢}{S}\in \mathrm{V}\to \left({S}\in \mathrm{UMGraph}↔\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)⟶\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
21 15 20 mp1i ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to \left({S}\in \mathrm{UMGraph}↔\left({{E}↾}_{{F}}\right):\mathrm{dom}\left({{E}↾}_{{F}}\right)⟶\left\{{p}\in 𝒫\left({V}\setminus \left\{{N}\right\}\right)|\left|{p}\right|=2\right\}\right)$
22 13 21 mpbird ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {N}\in {V}\right)\to {S}\in \mathrm{UMGraph}$