dlwwlknondlwlknonf1o

Description: F is a bijection between the two representations of double loops of a fixed positive length on a fixed vertex. (Contributed by AV, 30-May-2022) (Revised by AV, 1-Nov-2022)

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

Proof

Step	Hyp	Ref	Expression
1		dlwwlknondlwlknonbij.v	$⊢ V = Vtx (G)$
2		dlwwlknondlwlknonbij.w	$⊢ W = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\}$
3		dlwwlknondlwlknonbij.d	$⊢ D = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
4		dlwwlknondlwlknonf1o.f	$⊢ F = (c \in W ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
5		df-3an	$⊢ (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X) \leftrightarrow ((\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X) \land 2^{nd} (w) (N - 2) = X)$
6	5	rabbii	$⊢ \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X \land 2^{nd} (w) (N - 2) = X)\} = \{w \in ClWalks (G) \| ((\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X) \land 2^{nd} (w) (N - 2) = X)\}$
7	2 6	eqtri	$⊢ W = \{w \in ClWalks (G) \| ((\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X) \land 2^{nd} (w) (N - 2) = X)\}$
8		eqid	$⊢ \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} = \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\}$
9		eqid	$⊢ (c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) = (c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|)$
10		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
11	1 8 9	clwwlknonclwlknonf1o	$⊢ (G \in USHGraph \land X \in V \land N \in ℕ) \to (c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$
12	10 11	syl3an3	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to (c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} ⟼ 2^{nd} (c) prefix \|1^{st} (c)\|) : \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$
13		fveq1	$⊢ y = 2^{nd} (c) prefix \|1^{st} (c)\| \to y (N - 2) = (2^{nd} (c) prefix \|1^{st} (c)\|) (N - 2)$
14	13	3ad2ant3	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \land y = 2^{nd} (c) prefix \|1^{st} (c)\|) \to y (N - 2) = (2^{nd} (c) prefix \|1^{st} (c)\|) (N - 2)$
15		2fveq3	$⊢ w = c \to \|1^{st} (w)\| = \|1^{st} (c)\|$
16	15	eqeq1d	$⊢ w = c \to (\|1^{st} (w)\| = N \leftrightarrow \|1^{st} (c)\| = N)$
17		fveq2	$⊢ w = c \to 2^{nd} (w) = 2^{nd} (c)$
18	17	fveq1d	$⊢ w = c \to 2^{nd} (w) (0) = 2^{nd} (c) (0)$
19	18	eqeq1d	$⊢ w = c \to (2^{nd} (w) (0) = X \leftrightarrow 2^{nd} (c) (0) = X)$
20	16 19	anbi12d	$⊢ w = c \to ((\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X) \leftrightarrow (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X))$
21	20	elrab	$⊢ c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \leftrightarrow (c \in ClWalks (G) \land (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X))$
22		simplrl	$⊢ ((c \in ClWalks (G) \land (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X)) \land (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2})) \to \|1^{st} (c)\| = N$
23		simpll	$⊢ ((c \in ClWalks (G) \land (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X)) \land (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2})) \to c \in ClWalks (G)$
24		simpr3	$⊢ ((c \in ClWalks (G) \land (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X)) \land (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2})) \to N \in ℤ_{\geq 2}$
25	22 23 24	3jca	$⊢ ((c \in ClWalks (G) \land (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X)) \land (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2})) \to (\|1^{st} (c)\| = N \land c \in ClWalks (G) \land N \in ℤ_{\geq 2})$
26	25	ex	$⊢ (c \in ClWalks (G) \land (\|1^{st} (c)\| = N \land 2^{nd} (c) (0) = X)) \to ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to (\|1^{st} (c)\| = N \land c \in ClWalks (G) \land N \in ℤ_{\geq 2}))$
27	21 26	sylbi	$⊢ c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \to ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to (\|1^{st} (c)\| = N \land c \in ClWalks (G) \land N \in ℤ_{\geq 2}))$
28	27	impcom	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\}) \to (\|1^{st} (c)\| = N \land c \in ClWalks (G) \land N \in ℤ_{\geq 2})$
29		dlwwlknondlwlknonf1olem1	$⊢ (\|1^{st} (c)\| = N \land c \in ClWalks (G) \land N \in ℤ_{\geq 2}) \to (2^{nd} (c) prefix \|1^{st} (c)\|) (N - 2) = 2^{nd} (c) (N - 2)$
30	28 29	syl	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\}) \to (2^{nd} (c) prefix \|1^{st} (c)\|) (N - 2) = 2^{nd} (c) (N - 2)$
31	30	3adant3	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \land y = 2^{nd} (c) prefix \|1^{st} (c)\|) \to (2^{nd} (c) prefix \|1^{st} (c)\|) (N - 2) = 2^{nd} (c) (N - 2)$
32	14 31	eqtrd	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \land y = 2^{nd} (c) prefix \|1^{st} (c)\|) \to y (N - 2) = 2^{nd} (c) (N - 2)$
33	32	eqeq1d	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \land y = 2^{nd} (c) prefix \|1^{st} (c)\|) \to (y (N - 2) = X \leftrightarrow 2^{nd} (c) (N - 2) = X)$
34		nfv	$⊢ Ⅎ w 2^{nd} (c) (N - 2) = X$
35	17	fveq1d	$⊢ w = c \to 2^{nd} (w) (N - 2) = 2^{nd} (c) (N - 2)$
36	35	eqeq1d	$⊢ w = c \to (2^{nd} (w) (N - 2) = X \leftrightarrow 2^{nd} (c) (N - 2) = X)$
37	34 36	sbiev	$⊢ [c/ w] 2^{nd} (w) (N - 2) = X \leftrightarrow 2^{nd} (c) (N - 2) = X$
38	33 37	bitr4di	$⊢ ((G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \land c \in \{w \in ClWalks (G) \| (\|1^{st} (w)\| = N \land 2^{nd} (w) (0) = X)\} \land y = 2^{nd} (c) prefix \|1^{st} (c)\|) \to (y (N - 2) = X \leftrightarrow [c/ w] 2^{nd} (w) (N - 2) = X)$
39	7 8 4 9 12 38	f1ossf1o	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to F : W \underset{1-1 onto}{⟶} \{y \in (X ClWWalksNOn (G) N) \| y (N - 2) = X\}$
40		fveq1	$⊢ w = y \to w (N - 2) = y (N - 2)$
41	40	eqeq1d	$⊢ w = y \to (w (N - 2) = X \leftrightarrow y (N - 2) = X)$
42	41	cbvrabv	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} = \{y \in (X ClWWalksNOn (G) N) \| y (N - 2) = X\}$
43	3 42	eqtri	$⊢ D = \{y \in (X ClWWalksNOn (G) N) \| y (N - 2) = X\}$
44		f1oeq3	$⊢ D = \{y \in (X ClWWalksNOn (G) N) \| y (N - 2) = X\} \to (F : W \underset{1-1 onto}{⟶} D \leftrightarrow F : W \underset{1-1 onto}{⟶} \{y \in (X ClWWalksNOn (G) N) \| y (N - 2) = X\})$
45	43 44	ax-mp	$⊢ F : W \underset{1-1 onto}{⟶} D \leftrightarrow F : W \underset{1-1 onto}{⟶} \{y \in (X ClWWalksNOn (G) N) \| y (N - 2) = X\}$
46	39 45	sylibr	$⊢ (G \in USHGraph \land X \in V \land N \in ℤ_{\geq 2}) \to F : W \underset{1-1 onto}{⟶} D$

Metamath Proof Explorer

Theorem dlwwlknondlwlknonf1o

Proof