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=V0AB1AB
Assertion umgr2v2evd2 VWAVBVABVtxDegGA=2

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g G=V0AB1AB
2 1 umgr2v2e VWAVBVABGUMGraph
3 1 umgr2v2evtxel VWAVAVtxG
4 3 3adant3 VWAVBVAVtxG
5 4 adantr VWAVBVABAVtxG
6 eqid VtxG=VtxG
7 eqid iEdgG=iEdgG
8 eqid domiEdgG=domiEdgG
9 eqid VtxDegG=VtxDegG
10 6 7 8 9 vtxdumgrval GUMGraphAVtxGVtxDegGA=xdomiEdgG|AiEdgGx
11 2 5 10 syl2anc VWAVBVABVtxDegGA=xdomiEdgG|AiEdgGx
12 1 umgr2v2eiedg VWAVBViEdgG=0AB1AB
13 12 dmeqd VWAVBVdomiEdgG=dom0AB1AB
14 prex ABV
15 14 14 dmprop dom0AB1AB=01
16 13 15 eqtrdi VWAVBVdomiEdgG=01
17 12 fveq1d VWAVBViEdgGx=0AB1ABx
18 17 eleq2d VWAVBVAiEdgGxA0AB1ABx
19 16 18 rabeqbidv VWAVBVxdomiEdgG|AiEdgGx=x01|A0AB1ABx
20 19 fveq2d VWAVBVxdomiEdgG|AiEdgGx=x01|A0AB1ABx
21 prid1g AVAAB
22 0ne1 01
23 c0ex 0V
24 23 14 fvpr1 010AB1AB0=AB
25 22 24 ax-mp 0AB1AB0=AB
26 21 25 eleqtrrdi AVA0AB1AB0
27 1ex 1V
28 27 14 fvpr2 010AB1AB1=AB
29 22 28 ax-mp 0AB1AB1=AB
30 21 29 eleqtrrdi AVA0AB1AB1
31 fveq2 x=00AB1ABx=0AB1AB0
32 31 eleq2d x=0A0AB1ABxA0AB1AB0
33 fveq2 x=10AB1ABx=0AB1AB1
34 33 eleq2d x=1A0AB1ABxA0AB1AB1
35 23 27 32 34 ralpr x01A0AB1ABxA0AB1AB0A0AB1AB1
36 26 30 35 sylanbrc AVx01A0AB1ABx
37 rabid2 01=x01|A0AB1ABxx01A0AB1ABx
38 36 37 sylibr AV01=x01|A0AB1ABx
39 38 eqcomd AVx01|A0AB1ABx=01
40 39 fveq2d AVx01|A0AB1ABx=01
41 prhash2ex 01=2
42 40 41 eqtrdi AVx01|A0AB1ABx=2
43 42 3ad2ant2 VWAVBVx01|A0AB1ABx=2
44 20 43 eqtrd VWAVBVxdomiEdgG|AiEdgGx=2
45 44 adantr VWAVBVABxdomiEdgG|AiEdgGx=2
46 11 45 eqtrd VWAVBVABVtxDegGA=2