clwwlknonclwlknonf1o

Description: F is a bijection between the two representations of closed walks of a fixed positive length on a fixed vertex. (Contributed by AV, 26-May-2022) (Proof shortened by AV, 7-Aug-2022) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwwlknonclwlknonf1o.v	$⊢ V = Vtx (G)$
	clwwlknonclwlknonf1o.w	$⊢ W = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\}$
	clwwlknonclwlknonf1o.f	$⊢ F = (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
Assertion	clwwlknonclwlknonf1o	$⊢ (G \in USHGraph \land X \in V \land N \in ℕ) \to F : W \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$

Proof

Step	Hyp	Ref	Expression
1		clwwlknonclwlknonf1o.v	$⊢ V = Vtx (G)$
2		clwwlknonclwlknonf1o.w	$⊢ W = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\}$
3		clwwlknonclwlknonf1o.f	$⊢ F = (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
4		eqid	$⊢ \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} = \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}$
5		eqid	$⊢ (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) = (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
6		eqid	$⊢ 1^{st} (c) = 1^{st} (c)$
7		eqid	$⊢ 2^{nd} (c) = 2^{nd} (c)$
8	6 7 4 5	clwlknf1oclwwlkn	$⊢ (G \in USHGraph \land N \in ℕ) \to (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \underset{1-1 onto}{⟶} N ClWWalksN G$
9	8	3adant2	$⊢ (G \in USHGraph \land X \in V \land N \in ℕ) \to (c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \underset{1-1 onto}{⟶} N ClWWalksN G$
10		fveq1	$⊢ s = 2^{nd} (c) prefix \|1^{st} (c)\| \to s (0) = (2^{nd} (c) prefix \|1^{st} (c)\|) (0)$
11	10	3ad2ant3	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \land s = 2^{nd} (c) prefix \|1^{st} (c)\|) \to s (0) = (2^{nd} (c) prefix \|1^{st} (c)\|) (0)$
12		2fveq3	$⊢ w = c \to \|1^{st} (w)\| = \|1^{st} (c)\|$
13	12	eqeq1d	$⊢ w = c \to (\|1^{st} (w)\| = N \leftrightarrow \|1^{st} (c)\| = N)$
14	13	elrab	$⊢ c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \leftrightarrow (c \in ClWalks (G) \land \|1^{st} (c)\| = N)$
15		clwlkwlk	$⊢ c \in ClWalks (G) \to c \in Walks (G)$
16		wlkcpr	$⊢ c \in Walks (G) \leftrightarrow 1^{st} (c) Walks (G) 2^{nd} (c)$
17		eqid	$⊢ Vtx (G) = Vtx (G)$
18	17	wlkpwrd	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to 2^{nd} (c) \in Word Vtx (G)$
19	18	3ad2ant1	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to 2^{nd} (c) \in Word Vtx (G)$
20		elnnuz	$⊢ N \in ℕ \leftrightarrow N \in ℤ_{\geq 1}$
21		eluzfz2	$⊢ N \in ℤ_{\geq 1} \to N \in (1 \dots N)$
22	20 21	sylbi	$⊢ N \in ℕ \to N \in (1 \dots N)$
23		fzelp1	$⊢ N \in (1 \dots N) \to N \in (1 \dots N + 1)$
24	22 23	syl	$⊢ N \in ℕ \to N \in (1 \dots N + 1)$
25	24	3ad2ant3	$⊢ (G \in USHGraph \land X \in V \land N \in ℕ) \to N \in (1 \dots N + 1)$
26	25	3ad2ant3	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to N \in (1 \dots N + 1)$
27		id	$⊢ \|1^{st} (c)\| = N \to \|1^{st} (c)\| = N$
28		oveq1	$⊢ \|1^{st} (c)\| = N \to \|1^{st} (c)\| + 1 = N + 1$
29	28	oveq2d	$⊢ \|1^{st} (c)\| = N \to (1 \dots \|1^{st} (c)\| + 1) = (1 \dots N + 1)$
30	27 29	eleq12d	$⊢ \|1^{st} (c)\| = N \to (\|1^{st} (c)\| \in (1 \dots \|1^{st} (c)\| + 1) \leftrightarrow N \in (1 \dots N + 1))$
31	30	3ad2ant2	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to (\|1^{st} (c)\| \in (1 \dots \|1^{st} (c)\| + 1) \leftrightarrow N \in (1 \dots N + 1))$
32	26 31	mpbird	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to \|1^{st} (c)\| \in (1 \dots \|1^{st} (c)\| + 1)$
33		wlklenvp1	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to \|2^{nd} (c)\| = \|1^{st} (c)\| + 1$
34	33	oveq2d	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to (1 \dots \|2^{nd} (c)\|) = (1 \dots \|1^{st} (c)\| + 1)$
35	34	eleq2d	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to (\|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|) \leftrightarrow \|1^{st} (c)\| \in (1 \dots \|1^{st} (c)\| + 1))$
36	35	3ad2ant1	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to (\|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|) \leftrightarrow \|1^{st} (c)\| \in (1 \dots \|1^{st} (c)\| + 1))$
37	32 36	mpbird	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|)$
38	19 37	jca	$⊢ (1^{st} (c) Walks (G) 2^{nd} (c) \land \|1^{st} (c)\| = N \land (G \in USHGraph \land X \in V \land N \in ℕ)) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|))$
39	38	3exp	$⊢ 1^{st} (c) Walks (G) 2^{nd} (c) \to (\|1^{st} (c)\| = N \to ((G \in USHGraph \land X \in V \land N \in ℕ) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|))))$
40	16 39	sylbi	$⊢ c \in Walks (G) \to (\|1^{st} (c)\| = N \to ((G \in USHGraph \land X \in V \land N \in ℕ) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|))))$
41	15 40	syl	$⊢ c \in ClWalks (G) \to (\|1^{st} (c)\| = N \to ((G \in USHGraph \land X \in V \land N \in ℕ) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|))))$
42	41	imp	$⊢ (c \in ClWalks (G) \land \|1^{st} (c)\| = N) \to ((G \in USHGraph \land X \in V \land N \in ℕ) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|)))$
43	14 42	sylbi	$⊢ c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \to ((G \in USHGraph \land X \in V \land N \in ℕ) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|)))$
44	43	impcom	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}) \to (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|))$
45		pfxfv0	$⊢ (2^{nd} (c) \in Word Vtx (G) \land \|1^{st} (c)\| \in (1 \dots \|2^{nd} (c)\|)) \to (2^{nd} (c) prefix \|1^{st} (c)\|) (0) = 2^{nd} (c) (0)$
46	44 45	syl	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\}) \to (2^{nd} (c) prefix \|1^{st} (c)\|) (0) = 2^{nd} (c) (0)$
47	46	3adant3	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \land s = 2^{nd} (c) prefix \|1^{st} (c)\|) \to (2^{nd} (c) prefix \|1^{st} (c)\|) (0) = 2^{nd} (c) (0)$
48	11 47	eqtrd	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \land s = 2^{nd} (c) prefix \|1^{st} (c)\|) \to s (0) = 2^{nd} (c) (0)$
49	48	eqeq1d	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \land s = 2^{nd} (c) prefix \|1^{st} (c)\|) \to (s (0) = X \leftrightarrow 2^{nd} (c) (0) = X)$
50		nfv	$⊢ Ⅎ w 2^{nd} (c) (0) = X$
51		fveq2	$⊢ w = c \to 2^{nd} (w) = 2^{nd} (c)$
52	51	fveq1d	$⊢ w = c \to 2^{nd} (w) (0) = 2^{nd} (c) (0)$
53	52	eqeq1d	$⊢ w = c \to (2^{nd} (w) (0) = X \leftrightarrow 2^{nd} (c) (0) = X)$
54	50 53	sbiev	$⊢ [c/ w] 2^{nd} (w) (0) = X \leftrightarrow 2^{nd} (c) (0) = X$
55	49 54	bitr4di	$⊢ ((G \in USHGraph \land X \in V \land N \in ℕ) \land c \in \{w \in ClWalks (G) \| \|1^{st} (w)\| = N\} \land s = 2^{nd} (c) prefix \|1^{st} (c)\|) \to (s (0) = X \leftrightarrow [c/ w] 2^{nd} (w) (0) = X)$
56	2 4 3 5 9 55	f1ossf1o	$⊢ (G \in USHGraph \land X \in V \land N \in ℕ) \to F : W \underset{1-1 onto}{⟶} \{s \in (N ClWWalksN G) \| s (0) = X\}$
57		clwwlknon	$⊢ X ClWWalksNOn (G) N = \{s \in (N ClWWalksN G) \| s (0) = X\}$
58		f1oeq3	$⊢ X ClWWalksNOn (G) N = \{s \in (N ClWWalksN G) \| s (0) = X\} \to (F : W \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow F : W \underset{1-1 onto}{⟶} \{s \in (N ClWWalksN G) \| s (0) = X\})$
59	57 58	ax-mp	$⊢ F : W \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \leftrightarrow F : W \underset{1-1 onto}{⟶} \{s \in (N ClWWalksN G) \| s (0) = X\}$
60	56 59	sylibr	$⊢ (G \in USHGraph \land X \in V \land N \in ℕ) \to F : W \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$

Metamath Proof Explorer

Theorem clwwlknonclwlknonf1o

Proof