trlreslem

Description: Lemma for trlres . Formerly part of proof of eupthres . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 6-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

	Ref	Expression
Hypotheses	trlres.v	$⊢ V = Vtx (G)$
	trlres.i	$⊢ I = iEdg (G)$
	trlres.d	$⊢ φ \to F Trails (G) P$
	trlres.n	$⊢ φ \to N \in (0 ..^\|F\|)$
	trlres.h	$⊢ H = F prefix N$
Assertion	trlreslem	$⊢ φ \to H : (0 ..^\|H\|) \underset{1-1 onto}{⟶} dom ({I ↾}_{F [(0 ..^N)]})$

Proof

Step	Hyp	Ref	Expression
1		trlres.v	$⊢ V = Vtx (G)$
2		trlres.i	$⊢ I = iEdg (G)$
3		trlres.d	$⊢ φ \to F Trails (G) P$
4		trlres.n	$⊢ φ \to N \in (0 ..^\|F\|)$
5		trlres.h	$⊢ H = F prefix N$
6	2	trlf1	$⊢ F Trails (G) P \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
7	3 6	syl	$⊢ φ \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
8		elfzouz2	$⊢ N \in (0 ..^\|F\|) \to \|F\| \in ℤ_{\geq N}$
9		fzoss2	$⊢ \|F\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|F\|)$
10	4 8 9	3syl	$⊢ φ \to (0 ..^N) \subseteq (0 ..^\|F\|)$
11		f1ores	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land (0 ..^N) \subseteq (0 ..^\|F\|)) \to ({F ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} F [(0 ..^N)]$
12	7 10 11	syl2anc	$⊢ φ \to ({F ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} F [(0 ..^N)]$
13		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
14	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
15	3 13 14	3syl	$⊢ φ \to F \in Word dom I$
16		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
17	16 4	sseldi	$⊢ φ \to N \in (0 \dots \|F\|)$
18		pfxres	$⊢ (F \in Word dom I \land N \in (0 \dots \|F\|)) \to F prefix N = {F ↾}_{(0 ..^N)}$
19	15 17 18	syl2anc	$⊢ φ \to F prefix N = {F ↾}_{(0 ..^N)}$
20	5 19	syl5eq	$⊢ φ \to H = {F ↾}_{(0 ..^N)}$
21	5	fveq2i	$⊢ \|H\| = \|F prefix N\|$
22		elfzofz	$⊢ N \in (0 ..^\|F\|) \to N \in (0 \dots \|F\|)$
23	4 22	syl	$⊢ φ \to N \in (0 \dots \|F\|)$
24		pfxlen	$⊢ (F \in Word dom I \land N \in (0 \dots \|F\|)) \to \|F prefix N\| = N$
25	15 23 24	syl2anc	$⊢ φ \to \|F prefix N\| = N$
26	21 25	syl5eq	$⊢ φ \to \|H\| = N$
27	26	oveq2d	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N)$
28		wrdf	$⊢ F \in Word dom I \to F : (0 ..^\|F\|) ⟶ dom I$
29		fimass	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to F [(0 ..^N)] \subseteq dom I$
30	14 28 29	3syl	$⊢ F Walks (G) P \to F [(0 ..^N)] \subseteq dom I$
31	3 13 30	3syl	$⊢ φ \to F [(0 ..^N)] \subseteq dom I$
32		ssdmres	$⊢ F [(0 ..^N)] \subseteq dom I \leftrightarrow dom ({I ↾}_{F [(0 ..^N)]}) = F [(0 ..^N)]$
33	31 32	sylib	$⊢ φ \to dom ({I ↾}_{F [(0 ..^N)]}) = F [(0 ..^N)]$
34	20 27 33	f1oeq123d	$⊢ φ \to (H : (0 ..^\|H\|) \underset{1-1 onto}{⟶} dom ({I ↾}_{F [(0 ..^N)]}) \leftrightarrow ({F ↾}_{(0 ..^N)}) : (0 ..^N) \underset{1-1 onto}{⟶} F [(0 ..^N)])$
35	12 34	mpbird	$⊢ φ \to H : (0 ..^\|H\|) \underset{1-1 onto}{⟶} dom ({I ↾}_{F [(0 ..^N)]})$

Metamath Proof Explorer

Theorem trlreslem

Proof