efgs1b

Description: Every extension sequence ending in an irreducible word is trivial. (Contributed by Mario Carneiro, 1-Oct-2015)

	Ref	Expression
Hypotheses	efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
	efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
	efgred.d	⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
	efgred.s	⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
Assertion	efgs1b	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( 𝑆 ‘ 𝐴 ) ∈ 𝐷 ↔ ( ♯ ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
2		efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5		efgred.d	⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6		efgred.s	⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7		eldifn	⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) → ¬ ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
8	7 5	eleq2s	⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ 𝐷 → ¬ ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
9	1 2 3 4 5 6	efgsdm	⊢ ( 𝐴 ∈ dom 𝑆 ↔ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) ∧ ( 𝐴 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑎 ∈ ( 1 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐴 ‘ 𝑎 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( 𝑎 − 1 ) ) ) ) )
10	9	simp1bi	⊢ ( 𝐴 ∈ dom 𝑆 → 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) )
11		eldifsn	⊢ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) ↔ ( 𝐴 ∈ Word 𝑊 ∧ 𝐴 ≠ ∅ ) )
12		lennncl	⊢ ( ( 𝐴 ∈ Word 𝑊 ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
13	11 12	sylbi	⊢ ( 𝐴 ∈ ( Word 𝑊 ∖ { ∅ } ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
14	10 13	syl	⊢ ( 𝐴 ∈ dom 𝑆 → ( ♯ ‘ 𝐴 ) ∈ ℕ )
15		elnn1uz2	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) = 1 ∨ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) )
16	14 15	sylib	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐴 ) = 1 ∨ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) )
17	16	ord	⊢ ( 𝐴 ∈ dom 𝑆 → ( ¬ ( ♯ ‘ 𝐴 ) = 1 → ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) )
18	10	eldifad	⊢ ( 𝐴 ∈ dom 𝑆 → 𝐴 ∈ Word 𝑊 )
19	18	adantr	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → 𝐴 ∈ Word 𝑊 )
20		wrdf	⊢ ( 𝐴 ∈ Word 𝑊 → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
21	19 20	syl	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → 𝐴 : ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ⟶ 𝑊 )
22		1z	⊢ 1 ∈ ℤ
23		simpr	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) )
24		df-2	⊢ 2 = ( 1 + 1 )
25	24	fveq2i	⊢ ( ℤ_≥ ‘ 2 ) = ( ℤ_≥ ‘ ( 1 + 1 ) )
26	23 25	eleqtrdi	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ ( 1 + 1 ) ) )
27		eluzp1m1	⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ ( 1 + 1 ) ) ) → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
28	22 26 27	sylancr	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
29		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
30	28 29	eleqtrrdi	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
31		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
32	30 31	sylibr	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
33		fzoend	⊢ ( 0 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
34		elfzofz	⊢ ( ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) − 1 ) ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
35	32 33 34	3syl	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
36		eluzelz	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
37	36	adantl	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
38		fzoval	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℤ → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
39	37 38	syl	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( 0 ..^ ( ♯ ‘ 𝐴 ) ) = ( 0 ... ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
40	35 39	eleqtrrd	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
41	21 40	ffvelcdmd	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ 𝑊 )
42		uz2m1nn	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ )
43	1 2 3 4 5 6	efgsdmi	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ℕ ) → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
44	42 43	sylan2	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
45		fveq2	⊢ ( 𝑎 = ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
46	45	rneqd	⊢ ( 𝑎 = ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) → ran ( 𝑇 ‘ 𝑎 ) = ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) )
47	46	eliuni	⊢ ( ( ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ∈ 𝑊 ∧ ( 𝑆 ‘ 𝐴 ) ∈ ran ( 𝑇 ‘ ( 𝐴 ‘ ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 ) ) ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) )
48	41 44 47	syl2anc	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) )
49		fveq2	⊢ ( 𝑎 = 𝑥 → ( 𝑇 ‘ 𝑎 ) = ( 𝑇 ‘ 𝑥 ) )
50	49	rneqd	⊢ ( 𝑎 = 𝑥 → ran ( 𝑇 ‘ 𝑎 ) = ran ( 𝑇 ‘ 𝑥 ) )
51	50	cbviunv	⊢ ∪ 𝑎 ∈ 𝑊 ran ( 𝑇 ‘ 𝑎 ) = ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 )
52	48 51	eleqtrdi	⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
53	52	ex	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 2 ) → ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) )
54	17 53	syld	⊢ ( 𝐴 ∈ dom 𝑆 → ( ¬ ( ♯ ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) )
55	54	con1d	⊢ ( 𝐴 ∈ dom 𝑆 → ( ¬ ( 𝑆 ‘ 𝐴 ) ∈ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) → ( ♯ ‘ 𝐴 ) = 1 ) )
56	8 55	syl5	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( 𝑆 ‘ 𝐴 ) ∈ 𝐷 → ( ♯ ‘ 𝐴 ) = 1 ) )
57	9	simp2bi	⊢ ( 𝐴 ∈ dom 𝑆 → ( 𝐴 ‘ 0 ) ∈ 𝐷 )
58		oveq1	⊢ ( ( ♯ ‘ 𝐴 ) = 1 → ( ( ♯ ‘ 𝐴 ) − 1 ) = ( 1 − 1 ) )
59		1m1e0	⊢ ( 1 − 1 ) = 0
60	58 59	eqtrdi	⊢ ( ( ♯ ‘ 𝐴 ) = 1 → ( ( ♯ ‘ 𝐴 ) − 1 ) = 0 )
61	60	fveq2d	⊢ ( ( ♯ ‘ 𝐴 ) = 1 → ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ‘ 0 ) )
62	61	eleq1d	⊢ ( ( ♯ ‘ 𝐴 ) = 1 → ( ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∈ 𝐷 ↔ ( 𝐴 ‘ 0 ) ∈ 𝐷 ) )
63	57 62	syl5ibrcom	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐴 ) = 1 → ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∈ 𝐷 ) )
64	1 2 3 4 5 6	efgsval	⊢ ( 𝐴 ∈ dom 𝑆 → ( 𝑆 ‘ 𝐴 ) = ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
65	64	eleq1d	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( 𝑆 ‘ 𝐴 ) ∈ 𝐷 ↔ ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) ∈ 𝐷 ) )
66	63 65	sylibrd	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( ♯ ‘ 𝐴 ) = 1 → ( 𝑆 ‘ 𝐴 ) ∈ 𝐷 ) )
67	56 66	impbid	⊢ ( 𝐴 ∈ dom 𝑆 → ( ( 𝑆 ‘ 𝐴 ) ∈ 𝐷 ↔ ( ♯ ‘ 𝐴 ) = 1 ) )

Metamath Proof Explorer

Theorem efgs1b

Proof