Metamath Proof Explorer


Theorem umgr2v2eiedg

Description: The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g G = V 0 A B 1 A B
Assertion umgr2v2eiedg V W A V B V iEdg G = 0 A B 1 A B

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g G = V 0 A B 1 A B
2 1 fveq2i iEdg G = iEdg V 0 A B 1 A B
3 simp1 V W A V B V V W
4 prex 0 A B 1 A B V
5 opiedgfv V W 0 A B 1 A B V iEdg V 0 A B 1 A B = 0 A B 1 A B
6 3 4 5 sylancl V W A V B V iEdg V 0 A B 1 A B = 0 A B 1 A B
7 2 6 syl5eq V W A V B V iEdg G = 0 A B 1 A B