efgsdmi

Description: Property of the last link in the chain of extensions. (Contributed by Mario Carneiro, 29-Sep-2015)

	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	efgsdmi	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to S (F) \in ran T (F (\|F\| - 1 - 1))$

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	efgsval	$⊢ F \in dom S \to S (F) = F (\|F\| - 1)$
8	7	adantr	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to S (F) = F (\|F\| - 1)$
9		fveq2	$⊢ i = \|F\| - 1 \to F (i) = F (\|F\| - 1)$
10		fvoveq1	$⊢ i = \|F\| - 1 \to F (i - 1) = F (\|F\| - 1 - 1)$
11	10	fveq2d	$⊢ i = \|F\| - 1 \to T (F (i - 1)) = T (F (\|F\| - 1 - 1))$
12	11	rneqd	$⊢ i = \|F\| - 1 \to ran T (F (i - 1)) = ran T (F (\|F\| - 1 - 1))$
13	9 12	eleq12d	$⊢ i = \|F\| - 1 \to (F (i) \in ran T (F (i - 1)) \leftrightarrow F (\|F\| - 1) \in ran T (F (\|F\| - 1 - 1)))$
14	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)))$
15	14	simp3bi	$⊢ F \in dom S \to \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1))$
16	15	adantr	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to \forall i \in (1 ..^\|F\|) F (i) \in ran T (F (i - 1))$
17		simpr	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to \|F\| - 1 \in ℕ$
18		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
19	17 18	eleqtrdi	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to \|F\| - 1 \in ℤ_{\geq 1}$
20		eluzfz1	$⊢ \|F\| - 1 \in ℤ_{\geq 1} \to 1 \in (1 \dots \|F\| - 1)$
21	19 20	syl	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to 1 \in (1 \dots \|F\| - 1)$
22	14	simp1bi	$⊢ F \in dom S \to F \in (Word W ∖ \{\emptyset\})$
23	22	adantr	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to F \in (Word W ∖ \{\emptyset\})$
24	23	eldifad	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to F \in Word W$
25		lencl	$⊢ F \in Word W \to \|F\| \in ℕ_{0}$
26		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
27		fzoval	$⊢ \|F\| \in ℤ \to (1 ..^\|F\|) = (1 \dots \|F\| - 1)$
28	24 25 26 27	4syl	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to (1 ..^\|F\|) = (1 \dots \|F\| - 1)$
29	21 28	eleqtrrd	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to 1 \in (1 ..^\|F\|)$
30		fzoend	$⊢ 1 \in (1 ..^\|F\|) \to \|F\| - 1 \in (1 ..^\|F\|)$
31	29 30	syl	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to \|F\| - 1 \in (1 ..^\|F\|)$
32	13 16 31	rspcdva	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to F (\|F\| - 1) \in ran T (F (\|F\| - 1 - 1))$
33	8 32	eqeltrd	$⊢ (F \in dom S \land \|F\| - 1 \in ℕ) \to S (F) \in ran T (F (\|F\| - 1 - 1))$

Metamath Proof Explorer

Theorem efgsdmi

Proof