Step | Hyp | Ref
| Expression |
1 | | efgredlemd.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ dom 𝑆) |
2 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
3 | | efgval.r |
. . . . . . . . 9
⊢ ∼ = (
~FG ‘𝐼) |
4 | | efgval2.m |
. . . . . . . . 9
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
5 | | efgval2.t |
. . . . . . . . 9
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
6 | | efgred.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
7 | | efgred.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) |
8 | 2, 3, 4, 5, 6, 7 | efgsdm 19120 |
. . . . . . . 8
⊢ (𝐶 ∈ dom 𝑆 ↔ (𝐶 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐶‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐶))(𝐶‘𝑖) ∈ ran (𝑇‘(𝐶‘(𝑖 − 1))))) |
9 | 8 | simp1bi 1147 |
. . . . . . 7
⊢ (𝐶 ∈ dom 𝑆 → 𝐶 ∈ (Word 𝑊 ∖ {∅})) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (Word 𝑊 ∖ {∅})) |
11 | 10 | eldifad 3878 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Word 𝑊) |
12 | | efgredlem.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ dom 𝑆) |
13 | 2, 3, 4, 5, 6, 7 | efgsdm 19120 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1))))) |
14 | 13 | simp1bi 1147 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) |
16 | 15 | eldifad 3878 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Word 𝑊) |
17 | | wrdf 14074 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑊 → 𝐴:(0..^(♯‘𝐴))⟶𝑊) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴:(0..^(♯‘𝐴))⟶𝑊) |
19 | | fzossfz 13261 |
. . . . . . . . 9
⊢
(0..^((♯‘𝐴) − 1)) ⊆
(0...((♯‘𝐴)
− 1)) |
20 | | lencl 14088 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑊 → (♯‘𝐴) ∈
ℕ0) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
22 | 21 | nn0zd 12280 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐴) ∈
ℤ) |
23 | | fzoval 13244 |
. . . . . . . . . 10
⊢
((♯‘𝐴)
∈ ℤ → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1))) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(♯‘𝐴)) = (0...((♯‘𝐴) − 1))) |
25 | 19, 24 | sseqtrrid 3954 |
. . . . . . . 8
⊢ (𝜑 → (0..^((♯‘𝐴) − 1)) ⊆
(0..^(♯‘𝐴))) |
26 | | efgredlemb.k |
. . . . . . . . 9
⊢ 𝐾 = (((♯‘𝐴) − 1) −
1) |
27 | | efgredlem.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
28 | | efgredlem.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ dom 𝑆) |
29 | | efgredlem.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) |
30 | | efgredlem.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) |
31 | 2, 3, 4, 5, 6, 7, 27, 12, 28, 29, 30 | efgredlema 19130 |
. . . . . . . . . . 11
⊢ (𝜑 → (((♯‘𝐴) − 1) ∈ ℕ
∧ ((♯‘𝐵)
− 1) ∈ ℕ)) |
32 | 31 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
ℕ) |
33 | | fzo0end 13334 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
− 1) ∈ ℕ → (((♯‘𝐴) − 1) − 1) ∈
(0..^((♯‘𝐴)
− 1))) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((♯‘𝐴) − 1) − 1) ∈
(0..^((♯‘𝐴)
− 1))) |
35 | 26, 34 | eqeltrid 2842 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (0..^((♯‘𝐴) − 1))) |
36 | 25, 35 | sseldd 3902 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐴))) |
37 | 18, 36 | ffvelrnd 6905 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊) |
38 | 37 | s1cld 14160 |
. . . . 5
⊢ (𝜑 → 〈“(𝐴‘𝐾)”〉 ∈ Word 𝑊) |
39 | | eldifsn 4700 |
. . . . . . . 8
⊢ (𝐶 ∈ (Word 𝑊 ∖ {∅}) ↔ (𝐶 ∈ Word 𝑊 ∧ 𝐶 ≠ ∅)) |
40 | | lennncl 14089 |
. . . . . . . 8
⊢ ((𝐶 ∈ Word 𝑊 ∧ 𝐶 ≠ ∅) → (♯‘𝐶) ∈
ℕ) |
41 | 39, 40 | sylbi 220 |
. . . . . . 7
⊢ (𝐶 ∈ (Word 𝑊 ∖ {∅}) →
(♯‘𝐶) ∈
ℕ) |
42 | 10, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐶) ∈
ℕ) |
43 | | lbfzo0 13282 |
. . . . . 6
⊢ (0 ∈
(0..^(♯‘𝐶))
↔ (♯‘𝐶)
∈ ℕ) |
44 | 42, 43 | sylibr 237 |
. . . . 5
⊢ (𝜑 → 0 ∈
(0..^(♯‘𝐶))) |
45 | | ccatval1 14133 |
. . . . 5
⊢ ((𝐶 ∈ Word 𝑊 ∧ 〈“(𝐴‘𝐾)”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘𝐶))) → ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0) = (𝐶‘0)) |
46 | 11, 38, 44, 45 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0) = (𝐶‘0)) |
47 | 2, 3, 4, 5, 6, 7 | efgsdm 19120 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1))))) |
48 | 47 | simp1bi 1147 |
. . . . . . . . . 10
⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) |
49 | 28, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) |
50 | 49 | eldifad 3878 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Word 𝑊) |
51 | | wrdf 14074 |
. . . . . . . 8
⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(♯‘𝐵))⟶𝑊) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵:(0..^(♯‘𝐵))⟶𝑊) |
53 | | fzossfz 13261 |
. . . . . . . . 9
⊢
(0..^((♯‘𝐵) − 1)) ⊆
(0...((♯‘𝐵)
− 1)) |
54 | | lencl 14088 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Word 𝑊 → (♯‘𝐵) ∈
ℕ0) |
55 | 50, 54 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
56 | 55 | nn0zd 12280 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐵) ∈
ℤ) |
57 | | fzoval 13244 |
. . . . . . . . . 10
⊢
((♯‘𝐵)
∈ ℤ → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1))) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(♯‘𝐵)) = (0...((♯‘𝐵) − 1))) |
59 | 53, 58 | sseqtrrid 3954 |
. . . . . . . 8
⊢ (𝜑 → (0..^((♯‘𝐵) − 1)) ⊆
(0..^(♯‘𝐵))) |
60 | | efgredlemb.l |
. . . . . . . . 9
⊢ 𝐿 = (((♯‘𝐵) − 1) −
1) |
61 | 31 | simprd 499 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐵) − 1) ∈
ℕ) |
62 | | fzo0end 13334 |
. . . . . . . . . 10
⊢
(((♯‘𝐵)
− 1) ∈ ℕ → (((♯‘𝐵) − 1) − 1) ∈
(0..^((♯‘𝐵)
− 1))) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((♯‘𝐵) − 1) − 1) ∈
(0..^((♯‘𝐵)
− 1))) |
64 | 60, 63 | eqeltrid 2842 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0..^((♯‘𝐵) − 1))) |
65 | 59, 64 | sseldd 3902 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (0..^(♯‘𝐵))) |
66 | 52, 65 | ffvelrnd 6905 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊) |
67 | 66 | s1cld 14160 |
. . . . 5
⊢ (𝜑 → 〈“(𝐵‘𝐿)”〉 ∈ Word 𝑊) |
68 | | ccatval1 14133 |
. . . . 5
⊢ ((𝐶 ∈ Word 𝑊 ∧ 〈“(𝐵‘𝐿)”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(♯‘𝐶))) → ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0) = (𝐶‘0)) |
69 | 11, 67, 44, 68 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0) = (𝐶‘0)) |
70 | 46, 69 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)) |
71 | | fviss 6788 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
72 | 2, 71 | eqsstri 3935 |
. . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
73 | 72, 37 | sseldi 3899 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 × 2o)) |
74 | | lencl 14088 |
. . . . . . . 8
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2o) →
(♯‘(𝐴‘𝐾)) ∈
ℕ0) |
75 | 73, 74 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈
ℕ0) |
76 | 75 | nn0red 12151 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) ∈ ℝ) |
77 | | 2rp 12591 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
78 | | ltaddrp 12623 |
. . . . . 6
⊢
(((♯‘(𝐴‘𝐾)) ∈ ℝ ∧ 2 ∈
ℝ+) → (♯‘(𝐴‘𝐾)) < ((♯‘(𝐴‘𝐾)) + 2)) |
79 | 76, 77, 78 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐴‘𝐾)) < ((♯‘(𝐴‘𝐾)) + 2)) |
80 | 21 | nn0red 12151 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℝ) |
81 | 80 | lem1d 11765 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐴) − 1) ≤
(♯‘𝐴)) |
82 | | fznn 13180 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → (((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴))
↔ (((♯‘𝐴)
− 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))) |
83 | 22, 82 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴))
↔ (((♯‘𝐴)
− 1) ∈ ℕ ∧ ((♯‘𝐴) − 1) ≤ (♯‘𝐴)))) |
84 | 32, 81, 83 | mpbir2and 713 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴))) |
85 | 2, 3, 4, 5, 6, 7 | efgsres 19128 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈
(1...(♯‘𝐴)))
→ (𝐴 ↾
(0..^((♯‘𝐴)
− 1))) ∈ dom 𝑆) |
86 | 12, 84, 85 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ↾ (0..^((♯‘𝐴) − 1))) ∈ dom 𝑆) |
87 | 2, 3, 4, 5, 6, 7 | efgsval 19121 |
. . . . . . . 8
⊢ ((𝐴 ↾
(0..^((♯‘𝐴)
− 1))) ∈ dom 𝑆
→ (𝑆‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) = ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) −
1))) |
88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) −
1))) |
89 | | fz1ssfz0 13208 |
. . . . . . . . . . . . . 14
⊢
(1...(♯‘𝐴)) ⊆ (0...(♯‘𝐴)) |
90 | 89, 84 | sseldi 3899 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝐴) − 1) ∈
(0...(♯‘𝐴))) |
91 | | pfxres 14244 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈
(0...(♯‘𝐴)))
→ (𝐴 prefix
((♯‘𝐴) −
1)) = (𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) |
92 | 16, 90, 91 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 prefix ((♯‘𝐴) − 1)) = (𝐴 ↾ (0..^((♯‘𝐴) − 1)))) |
93 | 92 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) =
(♯‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1))))) |
94 | | pfxlen 14248 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑊 ∧ ((♯‘𝐴) − 1) ∈
(0...(♯‘𝐴)))
→ (♯‘(𝐴
prefix ((♯‘𝐴)
− 1))) = ((♯‘𝐴) − 1)) |
95 | 16, 90, 94 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐴 prefix ((♯‘𝐴) − 1))) =
((♯‘𝐴) −
1)) |
96 | 93, 95 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) = ((♯‘𝐴) − 1)) |
97 | 96 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) − 1) = (((♯‘𝐴) − 1) − 1)) |
98 | 97, 26 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝐴 ↾
(0..^((♯‘𝐴)
− 1)))) − 1) = 𝐾) |
99 | 98 | fveq2d 6721 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘((♯‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) − 1)) =
((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘𝐾)) |
100 | 35 | fvresd 6737 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘𝐾) = (𝐴‘𝐾)) |
101 | 88, 99, 100 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝐴‘𝐾)) |
102 | 101 | fveq2d 6721 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) =
(♯‘(𝐴‘𝐾))) |
103 | 2, 3, 4, 5, 6, 7 | efgsdmi 19122 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom 𝑆 ∧ ((♯‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) |
104 | 12, 32, 103 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1)))) |
105 | 26 | fveq2i 6720 |
. . . . . . . . 9
⊢ (𝐴‘𝐾) = (𝐴‘(((♯‘𝐴) − 1) − 1)) |
106 | 105 | fveq2i 6720 |
. . . . . . . 8
⊢ (𝑇‘(𝐴‘𝐾)) = (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) |
107 | 106 | rneqi 5806 |
. . . . . . 7
⊢ ran
(𝑇‘(𝐴‘𝐾)) = ran (𝑇‘(𝐴‘(((♯‘𝐴) − 1) − 1))) |
108 | 104, 107 | eleqtrrdi 2849 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘𝐾))) |
109 | 2, 3, 4, 5 | efgtlen 19116 |
. . . . . 6
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘𝐾))) → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘𝐾)) + 2)) |
110 | 37, 108, 109 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐴‘𝐾)) + 2)) |
111 | 79, 102, 110 | 3brtr4d 5085 |
. . . 4
⊢ (𝜑 → (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴))) |
112 | | efgredlemb.p |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (0...(♯‘(𝐴‘𝐾)))) |
113 | | efgredlemb.q |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ (0...(♯‘(𝐵‘𝐿)))) |
114 | | efgredlemb.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (𝐼 × 2o)) |
115 | | efgredlemb.v |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ (𝐼 × 2o)) |
116 | | efgredlemb.6 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) |
117 | | efgredlemb.7 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) |
118 | | efgredlemb.8 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) |
119 | | efgredlemd.9 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) |
120 | | efgredlemd.sc |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) prefix 𝑄) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (♯‘(𝐴‘𝐾))〉))) |
121 | 2, 3, 4, 5, 6, 7, 27, 12, 28, 29, 30, 26, 60, 112, 113, 114, 115, 116, 117, 118, 119, 1, 120 | efgredleme 19133 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))) |
122 | 121 | simpld 498 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) |
123 | 2, 3, 4, 5, 6, 7 | efgsp1 19127 |
. . . . . . 7
⊢ ((𝐶 ∈ dom 𝑆 ∧ (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) → (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) |
124 | 1, 122, 123 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) |
125 | 2, 3, 4, 5, 6, 7 | efgsval2 19123 |
. . . . . 6
⊢ ((𝐶 ∈ Word 𝑊 ∧ (𝐴‘𝐾) ∈ 𝑊 ∧ (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) → (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) = (𝐴‘𝐾)) |
126 | 11, 37, 124, 125 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) = (𝐴‘𝐾)) |
127 | 101, 126 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉))) |
128 | | 2fveq3 6722 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) →
(♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) −
1)))))) |
129 | 128 | breq1d 5063 |
. . . . . . 7
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) →
((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)))) |
130 | | fveqeq2 6726 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏))) |
131 | | fveq1 6716 |
. . . . . . . . 9
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((♯‘𝐴) −
1)))‘0)) |
132 | 131 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))) |
133 | 130, 132 | imbi12d 348 |
. . . . . . 7
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)))) |
134 | 129, 133 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = (𝐴 ↾ (0..^((♯‘𝐴) − 1))) →
(((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))))) |
135 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (𝑆‘𝑏) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉))) |
136 | 135 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)))) |
137 | | fveq1 6716 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (𝑏‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)) |
138 | 137 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾
(0..^((♯‘𝐴)
− 1)))‘0) = ((𝐶
++ 〈“(𝐴‘𝐾)”〉)‘0))) |
139 | 136, 138 | imbi12d 348 |
. . . . . . 7
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)))) |
140 | 139 | imbi2d 344 |
. . . . . 6
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) →
(((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝑏‘0))) ↔
((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0))))) |
141 | 134, 140 | rspc2va 3548 |
. . . . 5
⊢ ((((𝐴 ↾
(0..^((♯‘𝐴)
− 1))) ∈ dom 𝑆
∧ (𝐶 ++
〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)))) |
142 | 86, 124, 27, 141 | syl21anc 838 |
. . . 4
⊢ (𝜑 → ((♯‘(𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((♯‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)))) |
143 | 111, 127,
142 | mp2d 49 |
. . 3
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)) |
144 | 72, 66 | sseldi 3899 |
. . . . . . . 8
⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 × 2o)) |
145 | | lencl 14088 |
. . . . . . . 8
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2o) →
(♯‘(𝐵‘𝐿)) ∈
ℕ0) |
146 | 144, 145 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈
ℕ0) |
147 | 146 | nn0red 12151 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) ∈ ℝ) |
148 | | ltaddrp 12623 |
. . . . . 6
⊢
(((♯‘(𝐵‘𝐿)) ∈ ℝ ∧ 2 ∈
ℝ+) → (♯‘(𝐵‘𝐿)) < ((♯‘(𝐵‘𝐿)) + 2)) |
149 | 147, 77, 148 | sylancl 589 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐵‘𝐿)) < ((♯‘(𝐵‘𝐿)) + 2)) |
150 | 55 | nn0red 12151 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐵) ∈
ℝ) |
151 | 150 | lem1d 11765 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐵) − 1) ≤
(♯‘𝐵)) |
152 | | fznn 13180 |
. . . . . . . . . . 11
⊢
((♯‘𝐵)
∈ ℤ → (((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵))
↔ (((♯‘𝐵)
− 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵)))) |
153 | 56, 152 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵))
↔ (((♯‘𝐵)
− 1) ∈ ℕ ∧ ((♯‘𝐵) − 1) ≤ (♯‘𝐵)))) |
154 | 61, 151, 153 | mpbir2and 713 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵))) |
155 | 2, 3, 4, 5, 6, 7 | efgsres 19128 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈
(1...(♯‘𝐵)))
→ (𝐵 ↾
(0..^((♯‘𝐵)
− 1))) ∈ dom 𝑆) |
156 | 28, 154, 155 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ↾ (0..^((♯‘𝐵) − 1))) ∈ dom 𝑆) |
157 | 2, 3, 4, 5, 6, 7 | efgsval 19121 |
. . . . . . . 8
⊢ ((𝐵 ↾
(0..^((♯‘𝐵)
− 1))) ∈ dom 𝑆
→ (𝑆‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) = ((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) −
1))) |
158 | 156, 157 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = ((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) −
1))) |
159 | | fz1ssfz0 13208 |
. . . . . . . . . . . . . 14
⊢
(1...(♯‘𝐵)) ⊆ (0...(♯‘𝐵)) |
160 | 159, 154 | sseldi 3899 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝐵) − 1) ∈
(0...(♯‘𝐵))) |
161 | | pfxres 14244 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈
(0...(♯‘𝐵)))
→ (𝐵 prefix
((♯‘𝐵) −
1)) = (𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) |
162 | 50, 160, 161 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 prefix ((♯‘𝐵) − 1)) = (𝐵 ↾ (0..^((♯‘𝐵) − 1)))) |
163 | 162 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) =
(♯‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1))))) |
164 | | pfxlen 14248 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Word 𝑊 ∧ ((♯‘𝐵) − 1) ∈
(0...(♯‘𝐵)))
→ (♯‘(𝐵
prefix ((♯‘𝐵)
− 1))) = ((♯‘𝐵) − 1)) |
165 | 50, 160, 164 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘(𝐵 prefix ((♯‘𝐵) − 1))) =
((♯‘𝐵) −
1)) |
166 | 163, 165 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) = ((♯‘𝐵) − 1)) |
167 | 166 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) − 1) = (((♯‘𝐵) − 1) − 1)) |
168 | 167, 60 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝐵 ↾
(0..^((♯‘𝐵)
− 1)))) − 1) = 𝐿) |
169 | 168 | fveq2d 6721 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) −
1)))‘((♯‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) − 1)) =
((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘𝐿)) |
170 | 64 | fvresd 6737 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘𝐿) = (𝐵‘𝐿)) |
171 | 158, 169,
170 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝐵‘𝐿)) |
172 | 171 | fveq2d 6721 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) =
(♯‘(𝐵‘𝐿))) |
173 | 2, 3, 4, 5, 6, 7 | efgsdmi 19122 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom 𝑆 ∧ ((♯‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) |
174 | 28, 61, 173 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) |
175 | 29, 174 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1)))) |
176 | 60 | fveq2i 6720 |
. . . . . . . . 9
⊢ (𝐵‘𝐿) = (𝐵‘(((♯‘𝐵) − 1) − 1)) |
177 | 176 | fveq2i 6720 |
. . . . . . . 8
⊢ (𝑇‘(𝐵‘𝐿)) = (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) |
178 | 177 | rneqi 5806 |
. . . . . . 7
⊢ ran
(𝑇‘(𝐵‘𝐿)) = ran (𝑇‘(𝐵‘(((♯‘𝐵) − 1) − 1))) |
179 | 175, 178 | eleqtrrdi 2849 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐵‘𝐿))) |
180 | 2, 3, 4, 5 | efgtlen 19116 |
. . . . . 6
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐵‘𝐿))) → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐵‘𝐿)) + 2)) |
181 | 66, 179, 180 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑆‘𝐴)) = ((♯‘(𝐵‘𝐿)) + 2)) |
182 | 149, 172,
181 | 3brtr4d 5085 |
. . . 4
⊢ (𝜑 → (♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴))) |
183 | 121 | simprd 499 |
. . . . . . 7
⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) |
184 | 2, 3, 4, 5, 6, 7 | efgsp1 19127 |
. . . . . . 7
⊢ ((𝐶 ∈ dom 𝑆 ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) → (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) |
185 | 1, 183, 184 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) |
186 | 2, 3, 4, 5, 6, 7 | efgsval2 19123 |
. . . . . 6
⊢ ((𝐶 ∈ Word 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊 ∧ (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) → (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) = (𝐵‘𝐿)) |
187 | 11, 66, 185, 186 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) = (𝐵‘𝐿)) |
188 | 171, 187 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉))) |
189 | | 2fveq3 6722 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) →
(♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) −
1)))))) |
190 | 189 | breq1d 5063 |
. . . . . . 7
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) →
((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) ↔ (♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴)))) |
191 | | fveqeq2 6726 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘𝑏))) |
192 | | fveq1 6716 |
. . . . . . . . 9
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (𝑎‘0) = ((𝐵 ↾ (0..^((♯‘𝐵) −
1)))‘0)) |
193 | 192 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝑏‘0))) |
194 | 191, 193 | imbi12d 348 |
. . . . . . 7
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝑏‘0)))) |
195 | 190, 194 | imbi12d 348 |
. . . . . 6
⊢ (𝑎 = (𝐵 ↾ (0..^((♯‘𝐵) − 1))) →
(((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝑏‘0))))) |
196 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (𝑆‘𝑏) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉))) |
197 | 196 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)))) |
198 | | fveq1 6716 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (𝑏‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)) |
199 | 198 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝑏‘0) ↔ ((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘0) = ((𝐶
++ 〈“(𝐵‘𝐿)”〉)‘0))) |
200 | 197, 199 | imbi12d 348 |
. . . . . . 7
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) =
((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)))) |
201 | 200 | imbi2d 344 |
. . . . . 6
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) →
(((♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝑏‘0))) ↔
((♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) =
((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0))))) |
202 | 195, 201 | rspc2va 3548 |
. . . . 5
⊢ ((((𝐵 ↾
(0..^((♯‘𝐵)
− 1))) ∈ dom 𝑆
∧ (𝐶 ++
〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) =
((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)))) |
203 | 156, 185,
27, 202 | syl21anc 838 |
. . . 4
⊢ (𝜑 → ((♯‘(𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1))))) <
(♯‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((♯‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) =
((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)))) |
204 | 182, 188,
203 | mp2d 49 |
. . 3
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) =
((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)) |
205 | 70, 143, 204 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) =
((𝐵 ↾
(0..^((♯‘𝐵)
− 1)))‘0)) |
206 | | lbfzo0 13282 |
. . . 4
⊢ (0 ∈
(0..^((♯‘𝐴)
− 1)) ↔ ((♯‘𝐴) − 1) ∈
ℕ) |
207 | 32, 206 | sylibr 237 |
. . 3
⊢ (𝜑 → 0 ∈
(0..^((♯‘𝐴)
− 1))) |
208 | 207 | fvresd 6737 |
. 2
⊢ (𝜑 → ((𝐴 ↾ (0..^((♯‘𝐴) − 1)))‘0) = (𝐴‘0)) |
209 | | lbfzo0 13282 |
. . . 4
⊢ (0 ∈
(0..^((♯‘𝐵)
− 1)) ↔ ((♯‘𝐵) − 1) ∈
ℕ) |
210 | 61, 209 | sylibr 237 |
. . 3
⊢ (𝜑 → 0 ∈
(0..^((♯‘𝐵)
− 1))) |
211 | 210 | fvresd 6737 |
. 2
⊢ (𝜑 → ((𝐵 ↾ (0..^((♯‘𝐵) − 1)))‘0) = (𝐵‘0)) |
212 | 205, 208,
211 | 3eqtr3d 2785 |
1
⊢ (𝜑 → (𝐴‘0) = (𝐵‘0)) |