Metamath Proof Explorer

Theorem efgredlemg

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

Ref Expression
Hypotheses efgval.w ⊢W=I⁡WordI×2𝑜
efgval.r ⊢∼˙=~FG⁡I
efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
efgredlem.1 ⊢φ→∀a∈dom⁡S∀b∈dom⁡SS⁡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=PT⁡A⁡KU
efgredlemb.7 ⊢φ→S⁡B=QT⁡B⁡LV
Assertion efgredlemg ⊢φ→A⁡K=B⁡L

Proof

Step Hyp Ref Expression
1 efgval.w ⊢W=I⁡WordI×2𝑜
2 efgval.r ⊢∼˙=~FG⁡I
3 efgval2.m ⊢M=y∈I,z∈2𝑜⟼y1𝑜∖z
4 efgval2.t ⊢T=v∈W⟼n∈0…v,w∈I×2𝑜⟼vsplicenn⟨“wM⁡w”⟩
5 efgred.d ⊢D=W∖⋃x∈Wran⁡T⁡x
6 efgred.s ⊢S=m∈t∈WordW∖∅|t⁡0∈D∧∀k∈1..^tt⁡k∈ran⁡T⁡t⁡k−1⟼m⁡m−1
7 efgredlem.1 ⊢φ→∀a∈dom⁡S∀b∈dom⁡SS⁡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=PT⁡A⁡KU
19 efgredlemb.7 ⊢φ→S⁡B=QT⁡B⁡LV
20 fviss ⊢I⁡WordI×2𝑜⊆WordI×2𝑜
21 1 20 eqsstri ⊢W⊆WordI×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∈WordI×2𝑜
25 lencl ⊢A⁡K∈WordI×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∈WordI×2𝑜
30 lencl ⊢B⁡L∈WordI×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