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 \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to \forall x \in 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 \in UPGraph \land F EulerPaths (G) P) \to G \in UPGraph$
4		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
5	2	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
6	4 5	syl	$⊢ G \in UPGraph \to Fun iEdg (G)$
7	6	adantr	$⊢ (G \in UPGraph \land F EulerPaths (G) P) \to Fun iEdg (G)$
8		simpr	$⊢ (G \in UPGraph \land F EulerPaths (G) P) \to F EulerPaths (G) P$
9	1 2 3 7 8	eupth2	$⊢ (G \in UPGraph \land F EulerPaths (G) P) \to \{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = if (P (0) = P (\|F\|), \emptyset, \{P (0), P (\|F\|)\})$
10	9	3adant3	$⊢ (G \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to \{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = if (P (0) = P (\|F\|), \emptyset, \{P (0), P (\|F\|)\})$
11		crctprop	$⊢ F Circuits (G) P \to (F Trails (G) P \land P (0) = P (\|F\|))$
12	11	simprd	$⊢ F Circuits (G) P \to P (0) = P (\|F\|)$
13	12	3ad2ant3	$⊢ (G \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to P (0) = P (\|F\|)$
14	13	iftrued	$⊢ (G \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to if (P (0) = P (\|F\|), \emptyset, \{P (0), P (\|F\|)\}) = \emptyset$
15	14	eqeq2d	$⊢ (G \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to (\{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = if (P (0) = P (\|F\|), \emptyset, \{P (0), P (\|F\|)\}) \leftrightarrow \{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = \emptyset)$
16		rabeq0	$⊢ \{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = \emptyset \leftrightarrow \forall x \in V \neg \neg 2 ∥ VtxDeg (G) (x)$
17		notnotr	$⊢ \neg \neg 2 ∥ VtxDeg (G) (x) \to 2 ∥ VtxDeg (G) (x)$
18	17	ralimi	$⊢ \forall x \in V \neg \neg 2 ∥ VtxDeg (G) (x) \to \forall x \in V 2 ∥ VtxDeg (G) (x)$
19	16 18	sylbi	$⊢ \{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = \emptyset \to \forall x \in V 2 ∥ VtxDeg (G) (x)$
20	15 19	syl6bi	$⊢ (G \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to (\{x \in V \| \neg 2 ∥ VtxDeg (G) (x)\} = if (P (0) = P (\|F\|), \emptyset, \{P (0), P (\|F\|)\}) \to \forall x \in V 2 ∥ VtxDeg (G) (x))$
21	10 20	mpd	$⊢ (G \in UPGraph \land F EulerPaths (G) P \land F Circuits (G) P) \to \forall x \in V 2 ∥ VtxDeg (G) (x)$

Metamath Proof Explorer

Theorem eulercrct

Proof