Metamath Proof Explorer


Theorem eulercrct

Description: A pseudograph with an Eulerian circuit <. F , P >. (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypothesis eulerpathpr.v V = Vtx G
Assertion eulercrct G UPGraph F EulerPaths G P F Circuits G P x V 2 VtxDeg G x

Proof

Step Hyp Ref Expression
1 eulerpathpr.v V = Vtx G
2 eqid iEdg G = iEdg G
3 simpl G UPGraph F EulerPaths G P G UPGraph
4 upgruhgr G UPGraph G UHGraph
5 2 uhgrfun G UHGraph Fun iEdg G
6 4 5 syl G UPGraph Fun iEdg G
7 6 adantr G UPGraph F EulerPaths G P Fun iEdg G
8 simpr G UPGraph F EulerPaths G P F EulerPaths G P
9 1 2 3 7 8 eupth2 G UPGraph F EulerPaths G P x V | ¬ 2 VtxDeg G x = if P 0 = P F P 0 P F
10 9 3adant3 G UPGraph F EulerPaths G P F Circuits G P x V | ¬ 2 VtxDeg G x = if P 0 = P F P 0 P F
11 crctprop F Circuits G P F Trails G P P 0 = P F
12 11 simprd F Circuits G P P 0 = P F
13 12 3ad2ant3 G UPGraph F EulerPaths G P F Circuits G P P 0 = P F
14 13 iftrued G UPGraph F EulerPaths G P F Circuits G P if P 0 = P F P 0 P F =
15 14 eqeq2d G UPGraph F EulerPaths G P F Circuits G P x V | ¬ 2 VtxDeg G x = if P 0 = P F P 0 P F x V | ¬ 2 VtxDeg G x =
16 rabeq0 x V | ¬ 2 VtxDeg G x = x V ¬ ¬ 2 VtxDeg G x
17 notnotr ¬ ¬ 2 VtxDeg G x 2 VtxDeg G x
18 17 ralimi x V ¬ ¬ 2 VtxDeg G x x V 2 VtxDeg G x
19 16 18 sylbi x V | ¬ 2 VtxDeg G x = x V 2 VtxDeg G x
20 15 19 syl6bi G UPGraph F EulerPaths G P F Circuits G P x V | ¬ 2 VtxDeg G x = if P 0 = P F P 0 P F x V 2 VtxDeg G x
21 10 20 mpd G UPGraph F EulerPaths G P F Circuits G P x V 2 VtxDeg G x