efgs1b

Description: Every extension sequence ending in an irreducible word is trivial. (Contributed by Mario Carneiro, 1-Oct-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	efgs1b	$⊢ A \in dom S \to (S (A) \in D \leftrightarrow \|A\| = 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		eldifn	$⊢ S (A) \in (W ∖ ⋃_{x \in W} ran T (x)) \to \neg S (A) \in ⋃_{x \in W} ran T (x)$
8	7 5	eleq2s	$⊢ S (A) \in D \to \neg S (A) \in ⋃_{x \in W} ran T (x)$
9	1 2 3 4 5 6	efgsdm	$⊢ A \in dom S \leftrightarrow (A \in (Word W ∖ \{\emptyset\}) \land A (0) \in D \land \forall a \in (1 ..^\|A\|) A (a) \in ran T (A (a - 1)))$
10	9	simp1bi	$⊢ A \in dom S \to A \in (Word W ∖ \{\emptyset\})$
11		eldifsn	$⊢ A \in (Word W ∖ \{\emptyset\}) \leftrightarrow (A \in Word W \land A \neq \emptyset)$
12		lennncl	$⊢ (A \in Word W \land A \neq \emptyset) \to \|A\| \in ℕ$
13	11 12	sylbi	$⊢ A \in (Word W ∖ \{\emptyset\}) \to \|A\| \in ℕ$
14	10 13	syl	$⊢ A \in dom S \to \|A\| \in ℕ$
15		elnn1uz2	$⊢ \|A\| \in ℕ \leftrightarrow (\|A\| = 1 \lor \|A\| \in ℤ_{\geq 2})$
16	14 15	sylib	$⊢ A \in dom S \to (\|A\| = 1 \lor \|A\| \in ℤ_{\geq 2})$
17	16	ord	$⊢ A \in dom S \to (\neg \|A\| = 1 \to \|A\| \in ℤ_{\geq 2})$
18	10	eldifad	$⊢ A \in dom S \to A \in Word W$
19	18	adantr	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to A \in Word W$
20		wrdf	$⊢ A \in Word W \to A : (0 ..^\|A\|) ⟶ W$
21	19 20	syl	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to A : (0 ..^\|A\|) ⟶ W$
22		1z	$⊢ 1 \in ℤ$
23		simpr	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| \in ℤ_{\geq 2}$
24		df-2	$⊢ 2 = 1 + 1$
25	24	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
26	23 25	eleqtrdi	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| \in ℤ_{\geq (1 + 1)}$
27		eluzp1m1	$⊢ (1 \in ℤ \land \|A\| \in ℤ_{\geq (1 + 1)}) \to \|A\| - 1 \in ℤ_{\geq 1}$
28	22 26 27	sylancr	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| - 1 \in ℤ_{\geq 1}$
29		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
30	28 29	eleqtrrdi	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| - 1 \in ℕ$
31		lbfzo0	$⊢ 0 \in (0 ..^\|A\| - 1) \leftrightarrow \|A\| - 1 \in ℕ$
32	30 31	sylibr	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to 0 \in (0 ..^\|A\| - 1)$
33		fzoend	$⊢ 0 \in (0 ..^\|A\| - 1) \to \|A\| - 1 - 1 \in (0 ..^\|A\| - 1)$
34		elfzofz	$⊢ \|A\| - 1 - 1 \in (0 ..^\|A\| - 1) \to \|A\| - 1 - 1 \in (0 \dots \|A\| - 1)$
35	32 33 34	3syl	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| - 1 - 1 \in (0 \dots \|A\| - 1)$
36		eluzelz	$⊢ \|A\| \in ℤ_{\geq 2} \to \|A\| \in ℤ$
37	36	adantl	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| \in ℤ$
38		fzoval	$⊢ \|A\| \in ℤ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
39	37 38	syl	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
40	35 39	eleqtrrd	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to \|A\| - 1 - 1 \in (0 ..^\|A\|)$
41	21 40	ffvelcdmd	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to A (\|A\| - 1 - 1) \in W$
42		uz2m1nn	$⊢ \|A\| \in ℤ_{\geq 2} \to \|A\| - 1 \in ℕ$
43	1 2 3 4 5 6	efgsdmi	$⊢ (A \in dom S \land \|A\| - 1 \in ℕ) \to S (A) \in ran T (A (\|A\| - 1 - 1))$
44	42 43	sylan2	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to S (A) \in ran T (A (\|A\| - 1 - 1))$
45		fveq2	$⊢ a = A (\|A\| - 1 - 1) \to T (a) = T (A (\|A\| - 1 - 1))$
46	45	rneqd	$⊢ a = A (\|A\| - 1 - 1) \to ran T (a) = ran T (A (\|A\| - 1 - 1))$
47	46	eliuni	$⊢ (A (\|A\| - 1 - 1) \in W \land S (A) \in ran T (A (\|A\| - 1 - 1))) \to S (A) \in ⋃_{a \in W} ran T (a)$
48	41 44 47	syl2anc	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to S (A) \in ⋃_{a \in W} ran T (a)$
49		fveq2	$⊢ a = x \to T (a) = T (x)$
50	49	rneqd	$⊢ a = x \to ran T (a) = ran T (x)$
51	50	cbviunv	$⊢ ⋃_{a \in W} ran T (a) = ⋃_{x \in W} ran T (x)$
52	48 51	eleqtrdi	$⊢ (A \in dom S \land \|A\| \in ℤ_{\geq 2}) \to S (A) \in ⋃_{x \in W} ran T (x)$
53	52	ex	$⊢ A \in dom S \to (\|A\| \in ℤ_{\geq 2} \to S (A) \in ⋃_{x \in W} ran T (x))$
54	17 53	syld	$⊢ A \in dom S \to (\neg \|A\| = 1 \to S (A) \in ⋃_{x \in W} ran T (x))$
55	54	con1d	$⊢ A \in dom S \to (\neg S (A) \in ⋃_{x \in W} ran T (x) \to \|A\| = 1)$
56	8 55	syl5	$⊢ A \in dom S \to (S (A) \in D \to \|A\| = 1)$
57	9	simp2bi	$⊢ A \in dom S \to A (0) \in D$
58		oveq1	$⊢ \|A\| = 1 \to \|A\| - 1 = 1 - 1$
59		1m1e0	$⊢ 1 - 1 = 0$
60	58 59	eqtrdi	$⊢ \|A\| = 1 \to \|A\| - 1 = 0$
61	60	fveq2d	$⊢ \|A\| = 1 \to A (\|A\| - 1) = A (0)$
62	61	eleq1d	$⊢ \|A\| = 1 \to (A (\|A\| - 1) \in D \leftrightarrow A (0) \in D)$
63	57 62	syl5ibrcom	$⊢ A \in dom S \to (\|A\| = 1 \to A (\|A\| - 1) \in D)$
64	1 2 3 4 5 6	efgsval	$⊢ A \in dom S \to S (A) = A (\|A\| - 1)$
65	64	eleq1d	$⊢ A \in dom S \to (S (A) \in D \leftrightarrow A (\|A\| - 1) \in D)$
66	63 65	sylibrd	$⊢ A \in dom S \to (\|A\| = 1 \to S (A) \in D)$
67	56 66	impbid	$⊢ A \in dom S \to (S (A) \in D \leftrightarrow \|A\| = 1)$

Metamath Proof Explorer

Theorem efgs1b

Proof