Metamath Proof Explorer

Theorem efgredlemg

Description: Lemma for efgred . (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
efgredlemb.p ⊢ φ → P ∈ 0 … A ⁡ K
efgredlemb.q ⊢ φ → Q ∈ 0 … B ⁡ L
efgredlemb.u ⊢ φ → U ∈ I × 2 𝑜
efgredlemb.v ⊢ φ → V ∈ I × 2 𝑜
efgredlemb.6 ⊢ φ → S ⁡ A = P T ⁡ A ⁡ K U
efgredlemb.7 ⊢ φ → S ⁡ B = Q T ⁡ B ⁡ L V
Assertion efgredlemg ⊢ φ → A ⁡ K = B ⁡ L

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 efgredlemb.p ⊢ φ → P ∈ 0 … A ⁡ K
15 efgredlemb.q ⊢ φ → Q ∈ 0 … B ⁡ L
16 efgredlemb.u ⊢ φ → U ∈ I × 2 𝑜
17 efgredlemb.v ⊢ φ → V ∈ I × 2 𝑜
18 efgredlemb.6 ⊢ φ → S ⁡ A = P T ⁡ A ⁡ K U
19 efgredlemb.7 ⊢ φ → S ⁡ B = Q T ⁡ B ⁡ L V
20 fviss ⊢ I ⁡ Word I × 2 𝑜 ⊆ Word I × 2 𝑜
21 1 20 eqsstri ⊢ W ⊆ Word I × 2 𝑜
22 1 2 3 4 5 6 7 8 9 10 11 12 13 efgredlemf ⊢ φ → A ⁡ K ∈ W ∧ B ⁡ L ∈ W
23 22 simpld ⊢ φ → A ⁡ K ∈ W
24 21 23 sselid ⊢ φ → A ⁡ K ∈ Word I × 2 𝑜
25 lencl ⊢ A ⁡ K ∈ Word I × 2 𝑜 → A ⁡ K ∈ ℕ 0
26 24 25 syl ⊢ φ → A ⁡ K ∈ ℕ 0
27 26 nn0cnd ⊢ φ → A ⁡ K ∈ ℂ
28 22 simprd ⊢ φ → B ⁡ L ∈ W
29 21 28 sselid ⊢ φ → B ⁡ L ∈ Word I × 2 𝑜
30 lencl ⊢ B ⁡ L ∈ Word I × 2 𝑜 → B ⁡ L ∈ ℕ 0
31 29 30 syl ⊢ φ → B ⁡ L ∈ ℕ 0
32 31 nn0cnd ⊢ φ → B ⁡ L ∈ ℂ
33 2cnd ⊢ φ → 2 ∈ ℂ
34 1 2 3 4 5 6 7 8 9 10 11 efgredlema ⊢ φ → A − 1 ∈ ℕ ∧ B − 1 ∈ ℕ
35 34 simpld ⊢ φ → A − 1 ∈ ℕ
36 1 2 3 4 5 6 efgsdmi ⊢ A ∈ dom ⁡ S ∧ A − 1 ∈ ℕ → S ⁡ A ∈ ran ⁡ T ⁡ A ⁡ A - 1 - 1
37 8 35 36 syl2anc ⊢ φ → S ⁡ A ∈ ran ⁡ T ⁡ A ⁡ A - 1 - 1
38 12 fveq2i ⊢ A ⁡ K = A ⁡ A - 1 - 1
39 38 fveq2i ⊢ T ⁡ A ⁡ K = T ⁡ A ⁡ A - 1 - 1
40 39 rneqi ⊢ ran ⁡ T ⁡ A ⁡ K = ran ⁡ T ⁡ A ⁡ A - 1 - 1
41 37 40 eleqtrrdi ⊢ φ → S ⁡ A ∈ ran ⁡ T ⁡ A ⁡ K
42 1 2 3 4 efgtlen ⊢ A ⁡ K ∈ W ∧ S ⁡ A ∈ ran ⁡ T ⁡ A ⁡ K → S ⁡ A = A ⁡ K + 2
43 23 41 42 syl2anc ⊢ φ → S ⁡ A = A ⁡ K + 2
44 34 simprd ⊢ φ → B − 1 ∈ ℕ
45 1 2 3 4 5 6 efgsdmi ⊢ B ∈ dom ⁡ S ∧ B − 1 ∈ ℕ → S ⁡ B ∈ ran ⁡ T ⁡ B ⁡ B - 1 - 1
46 9 44 45 syl2anc ⊢ φ → S ⁡ B ∈ ran ⁡ T ⁡ B ⁡ B - 1 - 1
47 10 46 eqeltrd ⊢ φ → S ⁡ A ∈ ran ⁡ T ⁡ B ⁡ B - 1 - 1
48 13 fveq2i ⊢ B ⁡ L = B ⁡ B - 1 - 1
49 48 fveq2i ⊢ T ⁡ B ⁡ L = T ⁡ B ⁡ B - 1 - 1
50 49 rneqi ⊢ ran ⁡ T ⁡ B ⁡ L = ran ⁡ T ⁡ B ⁡ B - 1 - 1
51 47 50 eleqtrrdi ⊢ φ → S ⁡ A ∈ ran ⁡ T ⁡ B ⁡ L
52 1 2 3 4 efgtlen ⊢ B ⁡ L ∈ W ∧ S ⁡ A ∈ ran ⁡ T ⁡ B ⁡ L → S ⁡ A = B ⁡ L + 2
53 28 51 52 syl2anc ⊢ φ → S ⁡ A = B ⁡ L + 2
54 43 53 eqtr3d ⊢ φ → A ⁡ K + 2 = B ⁡ L + 2
55 27 32 33 54 addcan2ad ⊢ φ → A ⁡ K = B ⁡ L