clwlkclwwlkf1

Description: F is a one-to-one function from the nonempty closed walks into the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 29-Oct-2022)

	Ref	Expression
Hypotheses	clwlkclwwlkf.c	$⊢ C = \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
	clwlkclwwlkf.f	$⊢ F = (c \in C ⟼ 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1))$
Assertion	clwlkclwwlkf1	$⊢ G \in USHGraph \to F : C \underset{1-1}{⟶} ClWWalks (G)$

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	$⊢ C = \{w \in ClWalks (G) \| 1 \leq \|1^{st} (w)\|\}$
2		clwlkclwwlkf.f	$⊢ F = (c \in C ⟼ 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1))$
3	1 2	clwlkclwwlkf	$⊢ G \in USHGraph \to F : C ⟶ ClWWalks (G)$
4		fveq2	$⊢ c = x \to 2^{nd} (c) = 2^{nd} (x)$
5		2fveq3	$⊢ c = x \to \|2^{nd} (c)\| = \|2^{nd} (x)\|$
6	5	oveq1d	$⊢ c = x \to \|2^{nd} (c)\| - 1 = \|2^{nd} (x)\| - 1$
7	4 6	oveq12d	$⊢ c = x \to 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) = 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1)$
8		id	$⊢ x \in C \to x \in C$
9		ovexd	$⊢ x \in C \to 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) \in V$
10	2 7 8 9	fvmptd3	$⊢ x \in C \to F (x) = 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1)$
11		fveq2	$⊢ c = y \to 2^{nd} (c) = 2^{nd} (y)$
12		2fveq3	$⊢ c = y \to \|2^{nd} (c)\| = \|2^{nd} (y)\|$
13	12	oveq1d	$⊢ c = y \to \|2^{nd} (c)\| - 1 = \|2^{nd} (y)\| - 1$
14	11 13	oveq12d	$⊢ c = y \to 2^{nd} (c) prefix (\|2^{nd} (c)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)$
15		id	$⊢ y \in C \to y \in C$
16		ovexd	$⊢ y \in C \to 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1) \in V$
17	2 14 15 16	fvmptd3	$⊢ y \in C \to F (y) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)$
18	10 17	eqeqan12d	$⊢ (x \in C \land y \in C) \to (F (x) = F (y) \leftrightarrow 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1))$
19	18	adantl	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to (F (x) = F (y) \leftrightarrow 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1))$
20		simplrl	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to x \in C$
21		simplrr	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to y \in C$
22		eqid	$⊢ 1^{st} (x) = 1^{st} (x)$
23		eqid	$⊢ 2^{nd} (x) = 2^{nd} (x)$
24	1 22 23	clwlkclwwlkflem	$⊢ x \in C \to (1^{st} (x) Walks (G) 2^{nd} (x) \land 2^{nd} (x) (0) = 2^{nd} (x) (\|1^{st} (x)\|) \land \|1^{st} (x)\| \in ℕ)$
25		wlklenvm1	$⊢ 1^{st} (x) Walks (G) 2^{nd} (x) \to \|1^{st} (x)\| = \|2^{nd} (x)\| - 1$
26	25	eqcomd	$⊢ 1^{st} (x) Walks (G) 2^{nd} (x) \to \|2^{nd} (x)\| - 1 = \|1^{st} (x)\|$
27	26	3ad2ant1	$⊢ (1^{st} (x) Walks (G) 2^{nd} (x) \land 2^{nd} (x) (0) = 2^{nd} (x) (\|1^{st} (x)\|) \land \|1^{st} (x)\| \in ℕ) \to \|2^{nd} (x)\| - 1 = \|1^{st} (x)\|$
28	24 27	syl	$⊢ x \in C \to \|2^{nd} (x)\| - 1 = \|1^{st} (x)\|$
29	28	adantr	$⊢ (x \in C \land y \in C) \to \|2^{nd} (x)\| - 1 = \|1^{st} (x)\|$
30	29	oveq2d	$⊢ (x \in C \land y \in C) \to 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (x) prefix \|1^{st} (x)\|$
31		eqid	$⊢ 1^{st} (y) = 1^{st} (y)$
32		eqid	$⊢ 2^{nd} (y) = 2^{nd} (y)$
33	1 31 32	clwlkclwwlkflem	$⊢ y \in C \to (1^{st} (y) Walks (G) 2^{nd} (y) \land 2^{nd} (y) (0) = 2^{nd} (y) (\|1^{st} (y)\|) \land \|1^{st} (y)\| \in ℕ)$
34		wlklenvm1	$⊢ 1^{st} (y) Walks (G) 2^{nd} (y) \to \|1^{st} (y)\| = \|2^{nd} (y)\| - 1$
35	34	eqcomd	$⊢ 1^{st} (y) Walks (G) 2^{nd} (y) \to \|2^{nd} (y)\| - 1 = \|1^{st} (y)\|$
36	35	3ad2ant1	$⊢ (1^{st} (y) Walks (G) 2^{nd} (y) \land 2^{nd} (y) (0) = 2^{nd} (y) (\|1^{st} (y)\|) \land \|1^{st} (y)\| \in ℕ) \to \|2^{nd} (y)\| - 1 = \|1^{st} (y)\|$
37	33 36	syl	$⊢ y \in C \to \|2^{nd} (y)\| - 1 = \|1^{st} (y)\|$
38	37	adantl	$⊢ (x \in C \land y \in C) \to \|2^{nd} (y)\| - 1 = \|1^{st} (y)\|$
39	38	oveq2d	$⊢ (x \in C \land y \in C) \to 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1) = 2^{nd} (y) prefix \|1^{st} (y)\|$
40	30 39	eqeq12d	$⊢ (x \in C \land y \in C) \to (2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1) \leftrightarrow 2^{nd} (x) prefix \|1^{st} (x)\| = 2^{nd} (y) prefix \|1^{st} (y)\|)$
41	40	adantl	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to (2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1) \leftrightarrow 2^{nd} (x) prefix \|1^{st} (x)\| = 2^{nd} (y) prefix \|1^{st} (y)\|)$
42	41	biimpa	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to 2^{nd} (x) prefix \|1^{st} (x)\| = 2^{nd} (y) prefix \|1^{st} (y)\|$
43	20 21 42	3jca	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to (x \in C \land y \in C \land 2^{nd} (x) prefix \|1^{st} (x)\| = 2^{nd} (y) prefix \|1^{st} (y)\|)$
44	1 22 23 31 32	clwlkclwwlkf1lem2	$⊢ (x \in C \land y \in C \land 2^{nd} (x) prefix \|1^{st} (x)\| = 2^{nd} (y) prefix \|1^{st} (y)\|) \to (\|1^{st} (x)\| = \|1^{st} (y)\| \land \forall i \in (0 ..^\|1^{st} (x)\|) 2^{nd} (x) (i) = 2^{nd} (y) (i))$
45		simpl	$⊢ (\|1^{st} (x)\| = \|1^{st} (y)\| \land \forall i \in (0 ..^\|1^{st} (x)\|) 2^{nd} (x) (i) = 2^{nd} (y) (i)) \to \|1^{st} (x)\| = \|1^{st} (y)\|$
46	43 44 45	3syl	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to \|1^{st} (x)\| = \|1^{st} (y)\|$
47	1 22 23 31 32	clwlkclwwlkf1lem3	$⊢ (x \in C \land y \in C \land 2^{nd} (x) prefix \|1^{st} (x)\| = 2^{nd} (y) prefix \|1^{st} (y)\|) \to \forall i \in (0 \dots \|1^{st} (x)\|) 2^{nd} (x) (i) = 2^{nd} (y) (i)$
48	43 47	syl	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to \forall i \in (0 \dots \|1^{st} (x)\|) 2^{nd} (x) (i) = 2^{nd} (y) (i)$
49		simpl	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to G \in USHGraph$
50		wlkcpr	$⊢ x \in Walks (G) \leftrightarrow 1^{st} (x) Walks (G) 2^{nd} (x)$
51	50	biimpri	$⊢ 1^{st} (x) Walks (G) 2^{nd} (x) \to x \in Walks (G)$
52	51	3ad2ant1	$⊢ (1^{st} (x) Walks (G) 2^{nd} (x) \land 2^{nd} (x) (0) = 2^{nd} (x) (\|1^{st} (x)\|) \land \|1^{st} (x)\| \in ℕ) \to x \in Walks (G)$
53	24 52	syl	$⊢ x \in C \to x \in Walks (G)$
54		wlkcpr	$⊢ y \in Walks (G) \leftrightarrow 1^{st} (y) Walks (G) 2^{nd} (y)$
55	54	biimpri	$⊢ 1^{st} (y) Walks (G) 2^{nd} (y) \to y \in Walks (G)$
56	55	3ad2ant1	$⊢ (1^{st} (y) Walks (G) 2^{nd} (y) \land 2^{nd} (y) (0) = 2^{nd} (y) (\|1^{st} (y)\|) \land \|1^{st} (y)\| \in ℕ) \to y \in Walks (G)$
57	33 56	syl	$⊢ y \in C \to y \in Walks (G)$
58	53 57	anim12i	$⊢ (x \in C \land y \in C) \to (x \in Walks (G) \land y \in Walks (G))$
59	58	adantl	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to (x \in Walks (G) \land y \in Walks (G))$
60		eqidd	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to \|1^{st} (x)\| = \|1^{st} (x)\|$
61	49 59 60	3jca	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to (G \in USHGraph \land (x \in Walks (G) \land y \in Walks (G)) \land \|1^{st} (x)\| = \|1^{st} (x)\|)$
62	61	adantr	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to (G \in USHGraph \land (x \in Walks (G) \land y \in Walks (G)) \land \|1^{st} (x)\| = \|1^{st} (x)\|)$
63		uspgr2wlkeq	$⊢ (G \in USHGraph \land (x \in Walks (G) \land y \in Walks (G)) \land \|1^{st} (x)\| = \|1^{st} (x)\|) \to (x = y \leftrightarrow (\|1^{st} (x)\| = \|1^{st} (y)\| \land \forall i \in (0 \dots \|1^{st} (x)\|) 2^{nd} (x) (i) = 2^{nd} (y) (i)))$
64	62 63	syl	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to (x = y \leftrightarrow (\|1^{st} (x)\| = \|1^{st} (y)\| \land \forall i \in (0 \dots \|1^{st} (x)\|) 2^{nd} (x) (i) = 2^{nd} (y) (i)))$
65	46 48 64	mpbir2and	$⊢ ((G \in USHGraph \land (x \in C \land y \in C)) \land 2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1)) \to x = y$
66	65	ex	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to (2^{nd} (x) prefix (\|2^{nd} (x)\| - 1) = 2^{nd} (y) prefix (\|2^{nd} (y)\| - 1) \to x = y)$
67	19 66	sylbid	$⊢ (G \in USHGraph \land (x \in C \land y \in C)) \to (F (x) = F (y) \to x = y)$
68	67	ralrimivva	$⊢ G \in USHGraph \to \forall x \in C \forall y \in C (F (x) = F (y) \to x = y)$
69		dff13	$⊢ F : C \underset{1-1}{⟶} ClWWalks (G) \leftrightarrow (F : C ⟶ ClWWalks (G) \land \forall x \in C \forall y \in C (F (x) = F (y) \to x = y))$
70	3 68 69	sylanbrc	$⊢ G \in USHGraph \to F : C \underset{1-1}{⟶} ClWWalks (G)$

Metamath Proof Explorer

Theorem clwlkclwwlkf1

Proof