Metamath Proof Explorer


Theorem umgr2v2evd2

Description: In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g G = V 0 A B 1 A B
Assertion umgr2v2evd2 V W A V B V A B VtxDeg G A = 2

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g G = V 0 A B 1 A B
2 1 umgr2v2e V W A V B V A B G UMGraph
3 1 umgr2v2evtxel V W A V A Vtx G
4 3 3adant3 V W A V B V A Vtx G
5 4 adantr V W A V B V A B A Vtx G
6 eqid Vtx G = Vtx G
7 eqid iEdg G = iEdg G
8 eqid dom iEdg G = dom iEdg G
9 eqid VtxDeg G = VtxDeg G
10 6 7 8 9 vtxdumgrval G UMGraph A Vtx G VtxDeg G A = x dom iEdg G | A iEdg G x
11 2 5 10 syl2anc V W A V B V A B VtxDeg G A = x dom iEdg G | A iEdg G x
12 1 umgr2v2eiedg V W A V B V iEdg G = 0 A B 1 A B
13 12 dmeqd V W A V B V dom iEdg G = dom 0 A B 1 A B
14 prex A B V
15 14 14 dmprop dom 0 A B 1 A B = 0 1
16 13 15 eqtrdi V W A V B V dom iEdg G = 0 1
17 12 fveq1d V W A V B V iEdg G x = 0 A B 1 A B x
18 17 eleq2d V W A V B V A iEdg G x A 0 A B 1 A B x
19 16 18 rabeqbidv V W A V B V x dom iEdg G | A iEdg G x = x 0 1 | A 0 A B 1 A B x
20 19 fveq2d V W A V B V x dom iEdg G | A iEdg G x = x 0 1 | A 0 A B 1 A B x
21 prid1g A V A A B
22 0ne1 0 1
23 c0ex 0 V
24 23 14 fvpr1 0 1 0 A B 1 A B 0 = A B
25 22 24 ax-mp 0 A B 1 A B 0 = A B
26 21 25 eleqtrrdi A V A 0 A B 1 A B 0
27 1ex 1 V
28 27 14 fvpr2 0 1 0 A B 1 A B 1 = A B
29 22 28 ax-mp 0 A B 1 A B 1 = A B
30 21 29 eleqtrrdi A V A 0 A B 1 A B 1
31 fveq2 x = 0 0 A B 1 A B x = 0 A B 1 A B 0
32 31 eleq2d x = 0 A 0 A B 1 A B x A 0 A B 1 A B 0
33 fveq2 x = 1 0 A B 1 A B x = 0 A B 1 A B 1
34 33 eleq2d x = 1 A 0 A B 1 A B x A 0 A B 1 A B 1
35 23 27 32 34 ralpr x 0 1 A 0 A B 1 A B x A 0 A B 1 A B 0 A 0 A B 1 A B 1
36 26 30 35 sylanbrc A V x 0 1 A 0 A B 1 A B x
37 rabid2 0 1 = x 0 1 | A 0 A B 1 A B x x 0 1 A 0 A B 1 A B x
38 36 37 sylibr A V 0 1 = x 0 1 | A 0 A B 1 A B x
39 38 eqcomd A V x 0 1 | A 0 A B 1 A B x = 0 1
40 39 fveq2d A V x 0 1 | A 0 A B 1 A B x = 0 1
41 prhash2ex 0 1 = 2
42 40 41 eqtrdi A V x 0 1 | A 0 A B 1 A B x = 2
43 42 3ad2ant2 V W A V B V x 0 1 | A 0 A B 1 A B x = 2
44 20 43 eqtrd V W A V B V x dom iEdg G | A iEdg G x = 2
45 44 adantr V W A V B V A B x dom iEdg G | A iEdg G x = 2
46 11 45 eqtrd V W A V B V A B VtxDeg G A = 2