wlk2v2e

Description: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk. Notice that G is a simple graph (without loops) only if X =/= Y . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021)

	Ref	Expression
Hypotheses	wlk2v2e.i	$⊢ I = ⟨“ \{X, Y\} ”⟩$
	wlk2v2e.f	$⊢ F = ⟨“ 00 ”⟩$
	wlk2v2e.x	$⊢ X \in V$
	wlk2v2e.y	$⊢ Y \in V$
	wlk2v2e.p	$⊢ P = ⟨“ X Y X ”⟩$
	wlk2v2e.g	$⊢ G = ⟨\{X, Y\}, I⟩$
Assertion	wlk2v2e	$⊢ F Walks (G) P$

Proof

Step	Hyp	Ref	Expression
1		wlk2v2e.i	$⊢ I = ⟨“ \{X, Y\} ”⟩$
2		wlk2v2e.f	$⊢ F = ⟨“ 00 ”⟩$
3		wlk2v2e.x	$⊢ X \in V$
4		wlk2v2e.y	$⊢ Y \in V$
5		wlk2v2e.p	$⊢ P = ⟨“ X Y X ”⟩$
6		wlk2v2e.g	$⊢ G = ⟨\{X, Y\}, I⟩$
7	1	opeq2i	$⊢ ⟨\{X, Y\}, I⟩ = ⟨\{X, Y\}, ⟨“ \{X, Y\} ”⟩⟩$
8	6 7	eqtri	$⊢ G = ⟨\{X, Y\}, ⟨“ \{X, Y\} ”⟩⟩$
9		uspgr2v1e2w	$⊢ (X \in V \land Y \in V) \to ⟨\{X, Y\}, ⟨“ \{X, Y\} ”⟩⟩ \in USHGraph$
10	3 4 9	mp2an	$⊢ ⟨\{X, Y\}, ⟨“ \{X, Y\} ”⟩⟩ \in USHGraph$
11	8 10	eqeltri	$⊢ G \in USHGraph$
12		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
13	11 12	ax-mp	$⊢ G \in UPGraph$
14	1 2	wlk2v2elem1	$⊢ F \in Word dom I$
15	3	prid1	$⊢ X \in \{X, Y\}$
16	4	prid2	$⊢ Y \in \{X, Y\}$
17		s3cl	$⊢ (X \in \{X, Y\} \land Y \in \{X, Y\} \land X \in \{X, Y\}) \to ⟨“ X Y X ”⟩ \in Word \{X, Y\}$
18	15 16 15 17	mp3an	$⊢ ⟨“ X Y X ”⟩ \in Word \{X, Y\}$
19	5 18	eqeltri	$⊢ P \in Word \{X, Y\}$
20		wrdf	$⊢ P \in Word \{X, Y\} \to P : (0 ..^\|P\|) ⟶ \{X, Y\}$
21	19 20	ax-mp	$⊢ P : (0 ..^\|P\|) ⟶ \{X, Y\}$
22	5	fveq2i	$⊢ \|P\| = \|⟨“ X Y X ”⟩\|$
23		s3len	$⊢ \|⟨“ X Y X ”⟩\| = 3$
24	22 23	eqtr2i	$⊢ 3 = \|P\|$
25	24	oveq2i	$⊢ (0 ..^3) = (0 ..^\|P\|)$
26	25	feq2i	$⊢ P : (0 ..^3) ⟶ \{X, Y\} \leftrightarrow P : (0 ..^\|P\|) ⟶ \{X, Y\}$
27	21 26	mpbir	$⊢ P : (0 ..^3) ⟶ \{X, Y\}$
28	2	fveq2i	$⊢ \|F\| = \|⟨“ 00 ”⟩\|$
29		s2len	$⊢ \|⟨“ 00 ”⟩\| = 2$
30	28 29	eqtri	$⊢ \|F\| = 2$
31	30	oveq2i	$⊢ (0 \dots \|F\|) = (0 \dots 2)$
32		3z	$⊢ 3 \in ℤ$
33		fzoval	$⊢ 3 \in ℤ \to (0 ..^3) = (0 \dots 3 - 1)$
34	32 33	ax-mp	$⊢ (0 ..^3) = (0 \dots 3 - 1)$
35		3m1e2	$⊢ 3 - 1 = 2$
36	35	oveq2i	$⊢ (0 \dots 3 - 1) = (0 \dots 2)$
37	34 36	eqtr2i	$⊢ (0 \dots 2) = (0 ..^3)$
38	31 37	eqtri	$⊢ (0 \dots \|F\|) = (0 ..^3)$
39	38	feq2i	$⊢ P : (0 \dots \|F\|) ⟶ \{X, Y\} \leftrightarrow P : (0 ..^3) ⟶ \{X, Y\}$
40	27 39	mpbir	$⊢ P : (0 \dots \|F\|) ⟶ \{X, Y\}$
41	1 2 3 4 5	wlk2v2elem2	$⊢ \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}$
42	14 40 41	3pm3.2i	$⊢ (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ \{X, Y\} \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
43	6	fveq2i	$⊢ Vtx (G) = Vtx (⟨\{X, Y\}, I⟩)$
44		prex	$⊢ \{X, Y\} \in V$
45		s1cli	$⊢ ⟨“ \{X, Y\} ”⟩ \in Word V$
46	1 45	eqeltri	$⊢ I \in Word V$
47		opvtxfv	$⊢ (\{X, Y\} \in V \land I \in Word V) \to Vtx (⟨\{X, Y\}, I⟩) = \{X, Y\}$
48	44 46 47	mp2an	$⊢ Vtx (⟨\{X, Y\}, I⟩) = \{X, Y\}$
49	43 48	eqtr2i	$⊢ \{X, Y\} = Vtx (G)$
50	6	fveq2i	$⊢ iEdg (G) = iEdg (⟨\{X, Y\}, I⟩)$
51		opiedgfv	$⊢ (\{X, Y\} \in V \land I \in Word V) \to iEdg (⟨\{X, Y\}, I⟩) = I$
52	44 46 51	mp2an	$⊢ iEdg (⟨\{X, Y\}, I⟩) = I$
53	50 52	eqtr2i	$⊢ I = iEdg (G)$
54	49 53	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ \{X, Y\} \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
55	42 54	mpbiri	$⊢ G \in UPGraph \to F Walks (G) P$
56	13 55	ax-mp	$⊢ F Walks (G) P$

Metamath Proof Explorer

Theorem wlk2v2e

Proof