Metamath Proof Explorer

Theorem efgredlemf

Description: Lemma for efgredleme . (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
Assertion efgredlemf ⊢φ→A⁡K∈W∧B⁡L∈W

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 1 2 3 4 5 6 efgsdm ⊢A∈dom⁡S↔A∈WordW∖∅∧A⁡0∈D∧∀i∈1..^AA⁡i∈ran⁡T⁡A⁡i−1
15 14 simp1bi ⊢A∈dom⁡S→A∈WordW∖∅
16 8 15 syl ⊢φ→A∈WordW∖∅
17 16 eldifad ⊢φ→A∈WordW
18 wrdf ⊢A∈WordW→A:0..^A⟶W
19 17 18 syl ⊢φ→A:0..^A⟶W
20 fzossfz ⊢0..^A−1⊆0…A−1
21 lencl ⊢A∈WordW→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∈WordW∖∅∧B⁡0∈D∧∀i∈1..^BB⁡i∈ran⁡T⁡B⁡i−1
35 34 simp1bi ⊢B∈dom⁡S→B∈WordW∖∅
36 9 35 syl ⊢φ→B∈WordW∖∅
37 36 eldifad ⊢φ→B∈WordW
38 wrdf ⊢B∈WordW→B:0..^B⟶W
39 37 38 syl ⊢φ→B:0..^B⟶W
40 fzossfz ⊢0..^B−1⊆0…B−1
41 lencl ⊢B∈WordW→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