wlkiswwlks1

Description: The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018) (Revised by AV, 9-Apr-2021)

		Ref	Expression
	Assertion	wlkiswwlks1	$⊢ G \in UPGraph \to (F Walks (G) P \to P \in WWalks (G))$

Proof

Step	Hyp	Ref	Expression
1		wlkn0	$⊢ F Walks (G) P \to P \neq \emptyset$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3		eqid	$⊢ iEdg (G) = iEdg (G)$
4	2 3	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}))$
5		simpr	$⊢ ((G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \land P \neq \emptyset) \to P \neq \emptyset$
6		ffz0iswrd	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to P \in Word Vtx (G)$
7	6	3ad2ant2	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to P \in Word Vtx (G)$
8	7	ad2antlr	$⊢ ((G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \land P \neq \emptyset) \to P \in Word Vtx (G)$
9		upgruhgr	$⊢ G \in UPGraph \to G \in UHGraph$
10	3	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
11		funfn	$⊢ Fun iEdg (G) \leftrightarrow iEdg (G) Fn dom iEdg (G)$
12	11	biimpi	$⊢ Fun iEdg (G) \to iEdg (G) Fn dom iEdg (G)$
13	9 10 12	3syl	$⊢ G \in UPGraph \to iEdg (G) Fn dom iEdg (G)$
14	13	ad2antlr	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land G \in UPGraph) \land i \in (0 ..^\|F\|)) \to iEdg (G) Fn dom iEdg (G)$
15		wrdsymbcl	$⊢ (F \in Word dom iEdg (G) \land i \in (0 ..^\|F\|)) \to F (i) \in dom iEdg (G)$
16	15	ad4ant14	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land G \in UPGraph) \land i \in (0 ..^\|F\|)) \to F (i) \in dom iEdg (G)$
17		fnfvelrn	$⊢ (iEdg (G) Fn dom iEdg (G) \land F (i) \in dom iEdg (G)) \to iEdg (G) (F (i)) \in ran iEdg (G)$
18	14 16 17	syl2anc	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land G \in UPGraph) \land i \in (0 ..^\|F\|)) \to iEdg (G) (F (i)) \in ran iEdg (G)$
19		edgval	$⊢ Edg (G) = ran iEdg (G)$
20	18 19	eleqtrrdi	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land G \in UPGraph) \land i \in (0 ..^\|F\|)) \to iEdg (G) (F (i)) \in Edg (G)$
21		eleq1	$⊢ \{P (i), P (i + 1)\} = iEdg (G) (F (i)) \to (\{P (i), P (i + 1)\} \in Edg (G) \leftrightarrow iEdg (G) (F (i)) \in Edg (G))$
22	21	eqcoms	$⊢ iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \to (\{P (i), P (i + 1)\} \in Edg (G) \leftrightarrow iEdg (G) (F (i)) \in Edg (G))$
23	20 22	syl5ibrcom	$⊢ (((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land G \in UPGraph) \land i \in (0 ..^\|F\|)) \to (iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \to \{P (i), P (i + 1)\} \in Edg (G))$
24	23	ralimdva	$⊢ ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \land G \in UPGraph) \to (\forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \to \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G))$
25	24	ex	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (G \in UPGraph \to (\forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \to \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G)))$
26	25	com23	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (\forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \to (G \in UPGraph \to \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G)))$
27	26	3impia	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to (G \in UPGraph \to \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G))$
28	27	impcom	$⊢ (G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \to \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G)$
29		lencl	$⊢ F \in Word dom iEdg (G) \to \|F\| \in ℕ_{0}$
30		ffz0hash	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to \|P\| = \|F\| + 1$
31	30	ex	$⊢ \|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to \|P\| = \|F\| + 1)$
32		oveq1	$⊢ \|P\| = \|F\| + 1 \to \|P\| - 1 = \|F\| + 1 - 1$
33		nn0cn	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℂ$
34		pncan1	$⊢ \|F\| \in ℂ \to \|F\| + 1 - 1 = \|F\|$
35	33 34	syl	$⊢ \|F\| \in ℕ_{0} \to \|F\| + 1 - 1 = \|F\|$
36	32 35	sylan9eqr	$⊢ (\|F\| \in ℕ_{0} \land \|P\| = \|F\| + 1) \to \|P\| - 1 = \|F\|$
37	36	ex	$⊢ \|F\| \in ℕ_{0} \to (\|P\| = \|F\| + 1 \to \|P\| - 1 = \|F\|)$
38	31 37	syld	$⊢ \|F\| \in ℕ_{0} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to \|P\| - 1 = \|F\|)$
39	29 38	syl	$⊢ F \in Word dom iEdg (G) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to \|P\| - 1 = \|F\|)$
40	39	imp	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to \|P\| - 1 = \|F\|$
41	40	oveq2d	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (0 ..^\|P\| - 1) = (0 ..^\|F\|)$
42	41	raleqdv	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (\forall i \in (0 ..^\|P\| - 1) \{P (i), P (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G))$
43	42	3adant3	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to (\forall i \in (0 ..^\|P\| - 1) \{P (i), P (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G))$
44	43	adantl	$⊢ (G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \to (\forall i \in (0 ..^\|P\| - 1) \{P (i), P (i + 1)\} \in Edg (G) \leftrightarrow \forall i \in (0 ..^\|F\|) \{P (i), P (i + 1)\} \in Edg (G))$
45	28 44	mpbird	$⊢ (G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \to \forall i \in (0 ..^\|P\| - 1) \{P (i), P (i + 1)\} \in Edg (G)$
46	45	adantr	$⊢ ((G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \land P \neq \emptyset) \to \forall i \in (0 ..^\|P\| - 1) \{P (i), P (i + 1)\} \in Edg (G)$
47		eqid	$⊢ Edg (G) = Edg (G)$
48	2 47	iswwlks	$⊢ P \in WWalks (G) \leftrightarrow (P \neq \emptyset \land P \in Word Vtx (G) \land \forall i \in (0 ..^\|P\| - 1) \{P (i), P (i + 1)\} \in Edg (G))$
49	5 8 46 48	syl3anbrc	$⊢ ((G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \land P \neq \emptyset) \to P \in WWalks (G)$
50	49	ex	$⊢ (G \in UPGraph \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\})) \to (P \neq \emptyset \to P \in WWalks (G))$
51	50	ex	$⊢ G \in UPGraph \to ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to (P \neq \emptyset \to P \in WWalks (G)))$
52	4 51	sylbid	$⊢ G \in UPGraph \to (F Walks (G) P \to (P \neq \emptyset \to P \in WWalks (G)))$
53	1 52	mpdi	$⊢ G \in UPGraph \to (F Walks (G) P \to P \in WWalks (G))$

Metamath Proof Explorer

Theorem wlkiswwlks1

Proof