Metamath Proof Explorer


Theorem umgrun

Description: The union U of two multigraphs G and H with the same vertex set V is a multigraph with the vertex V and the union ( E u. F ) of the (indexed) edges. (Contributed by AV, 25-Nov-2020)

Ref Expression
Hypotheses umgrun.g φGUMGraph
umgrun.h φHUMGraph
umgrun.e E=iEdgG
umgrun.f F=iEdgH
umgrun.vg V=VtxG
umgrun.vh φVtxH=V
umgrun.i φdomEdomF=
umgrun.u φUW
umgrun.v φVtxU=V
umgrun.un φiEdgU=EF
Assertion umgrun φUUMGraph

Proof

Step Hyp Ref Expression
1 umgrun.g φGUMGraph
2 umgrun.h φHUMGraph
3 umgrun.e E=iEdgG
4 umgrun.f F=iEdgH
5 umgrun.vg V=VtxG
6 umgrun.vh φVtxH=V
7 umgrun.i φdomEdomF=
8 umgrun.u φUW
9 umgrun.v φVtxU=V
10 umgrun.un φiEdgU=EF
11 5 3 umgrf GUMGraphE:domEx𝒫V|x=2
12 1 11 syl φE:domEx𝒫V|x=2
13 eqid VtxH=VtxH
14 13 4 umgrf HUMGraphF:domFx𝒫VtxH|x=2
15 2 14 syl φF:domFx𝒫VtxH|x=2
16 6 eqcomd φV=VtxH
17 16 pweqd φ𝒫V=𝒫VtxH
18 17 rabeqdv φx𝒫V|x=2=x𝒫VtxH|x=2
19 18 feq3d φF:domFx𝒫V|x=2F:domFx𝒫VtxH|x=2
20 15 19 mpbird φF:domFx𝒫V|x=2
21 12 20 7 fun2d φEF:domEdomFx𝒫V|x=2
22 10 dmeqd φdomiEdgU=domEF
23 dmun domEF=domEdomF
24 22 23 eqtrdi φdomiEdgU=domEdomF
25 9 pweqd φ𝒫VtxU=𝒫V
26 25 rabeqdv φx𝒫VtxU|x=2=x𝒫V|x=2
27 10 24 26 feq123d φiEdgU:domiEdgUx𝒫VtxU|x=2EF:domEdomFx𝒫V|x=2
28 21 27 mpbird φiEdgU:domiEdgUx𝒫VtxU|x=2
29 eqid VtxU=VtxU
30 eqid iEdgU=iEdgU
31 29 30 isumgrs UWUUMGraphiEdgU:domiEdgUx𝒫VtxU|x=2
32 8 31 syl φUUMGraphiEdgU:domiEdgUx𝒫VtxU|x=2
33 28 32 mpbird φUUMGraph