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 φ G UMGraph
umgrun.h φ H UMGraph
umgrun.e E = iEdg G
umgrun.f F = iEdg H
umgrun.vg V = Vtx G
umgrun.vh φ Vtx H = V
umgrun.i φ dom E dom F =
umgrun.u φ U W
umgrun.v φ Vtx U = V
umgrun.un φ iEdg U = E F
Assertion umgrun φ U UMGraph

Proof

Step Hyp Ref Expression
1 umgrun.g φ G UMGraph
2 umgrun.h φ H UMGraph
3 umgrun.e E = iEdg G
4 umgrun.f F = iEdg H
5 umgrun.vg V = Vtx G
6 umgrun.vh φ Vtx H = V
7 umgrun.i φ dom E dom F =
8 umgrun.u φ U W
9 umgrun.v φ Vtx U = V
10 umgrun.un φ iEdg U = E F
11 5 3 umgrf G UMGraph E : dom E x 𝒫 V | x = 2
12 1 11 syl φ E : dom E x 𝒫 V | x = 2
13 eqid Vtx H = Vtx H
14 13 4 umgrf H UMGraph F : dom F x 𝒫 Vtx H | x = 2
15 2 14 syl φ F : dom F x 𝒫 Vtx H | x = 2
16 6 eqcomd φ V = Vtx H
17 16 pweqd φ 𝒫 V = 𝒫 Vtx H
18 17 rabeqdv φ x 𝒫 V | x = 2 = x 𝒫 Vtx H | x = 2
19 18 feq3d φ F : dom F x 𝒫 V | x = 2 F : dom F x 𝒫 Vtx H | x = 2
20 15 19 mpbird φ F : dom F x 𝒫 V | x = 2
21 12 20 7 fun2d φ E F : dom E dom F x 𝒫 V | x = 2
22 10 dmeqd φ dom iEdg U = dom E F
23 dmun dom E F = dom E dom F
24 22 23 eqtrdi φ dom iEdg U = dom E dom F
25 9 pweqd φ 𝒫 Vtx U = 𝒫 V
26 25 rabeqdv φ x 𝒫 Vtx U | x = 2 = x 𝒫 V | x = 2
27 10 24 26 feq123d φ iEdg U : dom iEdg U x 𝒫 Vtx U | x = 2 E F : dom E dom F x 𝒫 V | x = 2
28 21 27 mpbird φ iEdg U : dom iEdg U x 𝒫 Vtx U | x = 2
29 eqid Vtx U = Vtx U
30 eqid iEdg U = iEdg U
31 29 30 isumgrs U W U UMGraph iEdg U : dom iEdg U x 𝒫 Vtx U | x = 2
32 8 31 syl φ U UMGraph iEdg U : dom iEdg U x 𝒫 Vtx U | x = 2
33 28 32 mpbird φ U UMGraph