Metamath Proof Explorer

Theorem efgredlemf

Description: Lemma for efgredleme . (Contributed by Mario Carneiro, 4-Jun-2016)

Ref Expression
Hypotheses efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
efgredlem.1 ⊢ φ → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
efgredlem.2 ⊢ φ → A ∈ dom ⁡ S
efgredlem.3 ⊢ φ → B ∈ dom ⁡ S
efgredlem.4 ⊢ φ → S ⁡ A = S ⁡ B
efgredlem.5 ⊢ φ → ¬ A ⁡ 0 = B ⁡ 0
efgredlemb.k ⊢ K = A - 1 - 1
efgredlemb.l ⊢ L = B - 1 - 1
Assertion efgredlemf ⊢ φ → A ⁡ K ∈ W ∧ B ⁡ L ∈ W

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ W = I ⁡ Word I × 2 𝑜
2 efgval.r ⊢ ∼ ˙ = ~ FG ⁡ I
3 efgval2.m ⊢ M = y ∈ I , z ∈ 2 𝑜 ⟼ y 1 𝑜 ∖ z
4 efgval2.t ⊢ T = v ∈ W ⟼ n ∈ 0 … v , w ∈ I × 2 𝑜 ⟼ v splice n n ⟨“ w M ⁡ w ”⟩
5 efgred.d ⊢ D = W ∖ ⋃ x ∈ W ran ⁡ T ⁡ x
6 efgred.s ⊢ S = m ∈ t ∈ Word W ∖ ∅ | t ⁡ 0 ∈ D ∧ ∀ k ∈ 1 ..^ t t ⁡ k ∈ ran ⁡ T ⁡ t ⁡ k − 1 ⟼ m ⁡ m − 1
7 efgredlem.1 ⊢ φ → ∀ a ∈ dom ⁡ S ∀ b ∈ dom ⁡ S S ⁡ a < S ⁡ A → S ⁡ a = S ⁡ b → a ⁡ 0 = b ⁡ 0
8 efgredlem.2 ⊢ φ → A ∈ dom ⁡ S
9 efgredlem.3 ⊢ φ → B ∈ dom ⁡ S
10 efgredlem.4 ⊢ φ → S ⁡ A = S ⁡ B
11 efgredlem.5 ⊢ φ → ¬ A ⁡ 0 = B ⁡ 0
12 efgredlemb.k ⊢ K = A - 1 - 1
13 efgredlemb.l ⊢ L = B - 1 - 1
14 1 2 3 4 5 6 efgsdm ⊢ A ∈ dom ⁡ S ↔ A ∈ Word W ∖ ∅ ∧ A ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ A A ⁡ i ∈ ran ⁡ T ⁡ A ⁡ i − 1
15 14 simp1bi ⊢ A ∈ dom ⁡ S → A ∈ Word W ∖ ∅
16 8 15 syl ⊢ φ → A ∈ Word W ∖ ∅
17 16 eldifad ⊢ φ → A ∈ Word W
18 wrdf ⊢ A ∈ Word W → A : 0 ..^ A ⟶ W
19 17 18 syl ⊢ φ → A : 0 ..^ A ⟶ W
20 fzossfz ⊢ 0 ..^ A − 1 ⊆ 0 … A − 1
21 lencl ⊢ A ∈ Word W → A ∈ ℕ 0
22 17 21 syl ⊢ φ → A ∈ ℕ 0
23 22 nn0zd ⊢ φ → A ∈ ℤ
24 fzoval ⊢ A ∈ ℤ → 0 ..^ A = 0 … A − 1
25 23 24 syl ⊢ φ → 0 ..^ A = 0 … A − 1
26 20 25 sseqtrrid ⊢ φ → 0 ..^ A − 1 ⊆ 0 ..^ A
27 1 2 3 4 5 6 7 8 9 10 11 efgredlema ⊢ φ → A − 1 ∈ ℕ ∧ B − 1 ∈ ℕ
28 27 simpld ⊢ φ → A − 1 ∈ ℕ
29 fzo0end ⊢ A − 1 ∈ ℕ → A - 1 - 1 ∈ 0 ..^ A − 1
30 28 29 syl ⊢ φ → A - 1 - 1 ∈ 0 ..^ A − 1
31 12 30 eqeltrid ⊢ φ → K ∈ 0 ..^ A − 1
32 26 31 sseldd ⊢ φ → K ∈ 0 ..^ A
33 19 32 ffvelcdmd ⊢ φ → A ⁡ K ∈ W
34 1 2 3 4 5 6 efgsdm ⊢ B ∈ dom ⁡ S ↔ B ∈ Word W ∖ ∅ ∧ B ⁡ 0 ∈ D ∧ ∀ i ∈ 1 ..^ B B ⁡ i ∈ ran ⁡ T ⁡ B ⁡ i − 1
35 34 simp1bi ⊢ B ∈ dom ⁡ S → B ∈ Word W ∖ ∅
36 9 35 syl ⊢ φ → B ∈ Word W ∖ ∅
37 36 eldifad ⊢ φ → B ∈ Word W
38 wrdf ⊢ B ∈ Word W → B : 0 ..^ B ⟶ W
39 37 38 syl ⊢ φ → B : 0 ..^ B ⟶ W
40 fzossfz ⊢ 0 ..^ B − 1 ⊆ 0 … B − 1
41 lencl ⊢ B ∈ Word W → B ∈ ℕ 0
42 37 41 syl ⊢ φ → B ∈ ℕ 0
43 42 nn0zd ⊢ φ → B ∈ ℤ
44 fzoval ⊢ B ∈ ℤ → 0 ..^ B = 0 … B − 1
45 43 44 syl ⊢ φ → 0 ..^ B = 0 … B − 1
46 40 45 sseqtrrid ⊢ φ → 0 ..^ B − 1 ⊆ 0 ..^ B
47 fzo0end ⊢ B − 1 ∈ ℕ → B - 1 - 1 ∈ 0 ..^ B − 1
48 27 47 simpl2im ⊢ φ → B - 1 - 1 ∈ 0 ..^ B − 1
49 13 48 eqeltrid ⊢ φ → L ∈ 0 ..^ B − 1
50 46 49 sseldd ⊢ φ → L ∈ 0 ..^ B
51 39 50 ffvelcdmd ⊢ φ → B ⁡ L ∈ W
52 33 51 jca ⊢ φ → A ⁡ K ∈ W ∧ B ⁡ L ∈ W