efgsres

Description: An initial segment of an extension sequence is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 3-Nov-2022)

	Ref	Expression
Hypotheses	efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
Assertion	efgsres	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to {F ↾}_{(0 ..^N)} \in dom S$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
6		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
7	1 2 3 4 5 6	efgsdm	$⊢ F \in dom S \leftrightarrow (F \in (Word W ∖ \{\emptyset\}) \land F (0) \in D \land \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1)))$
8	7	simp1bi	$⊢ F \in dom S \to F \in (Word W ∖ \{\emptyset\})$
9	8	adantr	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to F \in (Word W ∖ \{\emptyset\})$
10	9	eldifad	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to F \in Word W$
11		fz1ssfz0	$⊢ (1 \dots \|F\|) \subseteq (0 \dots \|F\|)$
12		simpr	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to N \in (1 \dots \|F\|)$
13	11 12	sselid	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to N \in (0 \dots \|F\|)$
14		pfxres	$⊢ (F \in Word W \land N \in (0 \dots \|F\|)) \to F prefix N = {F ↾}_{(0 ..^N)}$
15	10 13 14	syl2anc	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to F prefix N = {F ↾}_{(0 ..^N)}$
16		pfxcl	$⊢ F \in Word W \to F prefix N \in Word W$
17	10 16	syl	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to F prefix N \in Word W$
18	15 17	eqeltrrd	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to {F ↾}_{(0 ..^N)} \in Word W$
19		pfxlen	$⊢ (F \in Word W \land N \in (0 \dots \|F\|)) \to \|F prefix N\| = N$
20	10 13 19	syl2anc	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \|F prefix N\| = N$
21		elfznn	$⊢ N \in (1 \dots \|F\|) \to N \in ℕ$
22	21	adantl	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to N \in ℕ$
23	20 22	eqeltrd	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \|F prefix N\| \in ℕ$
24		wrdfin	$⊢ F prefix N \in Word W \to F prefix N \in Fin$
25		hashnncl	$⊢ F prefix N \in Fin \to (\|F prefix N\| \in ℕ \leftrightarrow F prefix N \neq \emptyset)$
26	17 24 25	3syl	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to (\|F prefix N\| \in ℕ \leftrightarrow F prefix N \neq \emptyset)$
27	23 26	mpbid	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to F prefix N \neq \emptyset$
28	15 27	eqnetrrd	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to {F ↾}_{(0 ..^N)} \neq \emptyset$
29		eldifsn	$⊢ {F ↾}_{(0 ..^N)} \in (Word W ∖ \{\emptyset\}) \leftrightarrow ({F ↾}_{(0 ..^N)} \in Word W \land {F ↾}_{(0 ..^N)} \neq \emptyset)$
30	18 28 29	sylanbrc	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to {F ↾}_{(0 ..^N)} \in (Word W ∖ \{\emptyset\})$
31		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
32	22 31	sylibr	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to 0 \in (0 ..^N)$
33	32	fvresd	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to ({F ↾}_{(0 ..^N)}) (0) = F (0)$
34	7	simp2bi	$⊢ F \in dom S \to F (0) \in D$
35	34	adantr	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to F (0) \in D$
36	33 35	eqeltrd	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to ({F ↾}_{(0 ..^N)}) (0) \in D$
37		elfzuz3	$⊢ N \in (1 \dots \|F\|) \to \|F\| \in ℤ_{\geq N}$
38	37	adantl	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \|F\| \in ℤ_{\geq N}$
39		fzoss2	$⊢ \|F\| \in ℤ_{\geq N} \to (1 ..^N) \subseteq (1 ..^\|F\|)$
40	38 39	syl	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to (1 ..^N) \subseteq (1 ..^\|F\|)$
41	7	simp3bi	$⊢ F \in dom S \to \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1))$
42	41	adantr	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1))$
43		ssralv	$⊢ (1 ..^N) \subseteq (1 ..^\|F\|) \to (\forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1)) \to \forall i \in (1 ..^N) F (i) \in ran T (F (i - 1)))$
44	40 42 43	sylc	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \forall i \in (1 ..^N) F (i) \in ran T (F (i - 1))$
45		fzo0ss1	$⊢ (1 ..^N) \subseteq (0 ..^N)$
46	45	sseli	$⊢ i \in (1 ..^N) \to i \in (0 ..^N)$
47	46	fvresd	$⊢ i \in (1 ..^N) \to ({F ↾}_{(0 ..^N)}) (i) = F (i)$
48		elfzoel2	$⊢ i \in (1 ..^N) \to N \in ℤ$
49		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
50	48 49	syl	$⊢ i \in (1 ..^N) \to N - 1 \in ℤ$
51		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
52	48 51	syl	$⊢ i \in (1 ..^N) \to N \in ℤ_{\geq N}$
53	48	zcnd	$⊢ i \in (1 ..^N) \to N \in ℂ$
54		ax-1cn	$⊢ 1 \in ℂ$
55		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
56	53 54 55	sylancl	$⊢ i \in (1 ..^N) \to N - 1 + 1 = N$
57	56	fveq2d	$⊢ i \in (1 ..^N) \to ℤ_{\geq (N - 1 + 1)} = ℤ_{\geq N}$
58	52 57	eleqtrrd	$⊢ i \in (1 ..^N) \to N \in ℤ_{\geq (N - 1 + 1)}$
59		peano2uzr	$⊢ (N - 1 \in ℤ \land N \in ℤ_{\geq (N - 1 + 1)}) \to N \in ℤ_{\geq (N - 1)}$
60	50 58 59	syl2anc	$⊢ i \in (1 ..^N) \to N \in ℤ_{\geq (N - 1)}$
61		fzoss2	$⊢ N \in ℤ_{\geq (N - 1)} \to (0 ..^N - 1) \subseteq (0 ..^N)$
62	60 61	syl	$⊢ i \in (1 ..^N) \to (0 ..^N - 1) \subseteq (0 ..^N)$
63		elfzo1elm1fzo0	$⊢ i \in (1 ..^N) \to i - 1 \in (0 ..^N - 1)$
64	62 63	sseldd	$⊢ i \in (1 ..^N) \to i - 1 \in (0 ..^N)$
65	64	fvresd	$⊢ i \in (1 ..^N) \to ({F ↾}_{(0 ..^N)}) (i - 1) = F (i - 1)$
66	65	fveq2d	$⊢ i \in (1 ..^N) \to T (({F ↾}_{(0 ..^N)}) (i - 1)) = T (F (i - 1))$
67	66	rneqd	$⊢ i \in (1 ..^N) \to ran T (({F ↾}_{(0 ..^N)}) (i - 1)) = ran T (F (i - 1))$
68	47 67	eleq12d	$⊢ i \in (1 ..^N) \to (({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1)) \leftrightarrow F (i) \in ran T (F (i - 1)))$
69	68	ralbiia	$⊢ \forall i \in (1 ..^N) ({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1)) \leftrightarrow \forall i \in (1 ..^N) F (i) \in ran T (F (i - 1))$
70	44 69	sylibr	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \forall i \in (1 ..^N) ({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1))$
71	15	fveq2d	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \|F prefix N\| = \|{F ↾}_{(0 ..^N)}\|$
72	71 20	eqtr3d	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \|{F ↾}_{(0 ..^N)}\| = N$
73	72	oveq2d	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to (1 ..^\|{F ↾}_{(0 ..^N)}\|) = (1 ..^N)$
74	73	raleqdv	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to (\forall i \in (1 ..^\|{F ↾}_{(0 ..^N)}\|) ({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1)) \leftrightarrow \forall i \in (1 ..^N) ({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1)))$
75	70 74	mpbird	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to \forall i \in (1 ..^\|{F ↾}_{(0 ..^N)}\|) ({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1))$
76	1 2 3 4 5 6	efgsdm	$⊢ {F ↾}_{(0 ..^N)} \in dom S \leftrightarrow ({F ↾}_{(0 ..^N)} \in (Word W ∖ \{\emptyset\}) \land ({F ↾}_{(0 ..^N)}) (0) \in D \land \forall i \in (1 ..^\|{F ↾}_{(0 ..^N)}\|) ({F ↾}_{(0 ..^N)}) (i) \in ran T (({F ↾}_{(0 ..^N)}) (i - 1)))$
77	30 36 75 76	syl3anbrc	$⊢ (F \in dom S \land N \in (1 \dots \|F\|)) \to {F ↾}_{(0 ..^N)} \in dom S$

Metamath Proof Explorer

Theorem efgsres

Proof