Step | Hyp | Ref
| Expression |
1 | | efgredlemd.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ dom 𝑆) |
2 | | efgval.w |
. . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
3 | | efgval.r |
. . . . . . . . 9
⊢ ∼ = (
~FG ‘𝐼) |
4 | | efgval2.m |
. . . . . . . . 9
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
5 | | efgval2.t |
. . . . . . . . 9
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
6 | | efgred.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
7 | | efgred.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
8 | 2, 3, 4, 5, 6, 7 | efgsdm 17966 |
. . . . . . . 8
⊢ (𝐶 ∈ dom 𝑆 ↔ (𝐶 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐶‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐶))(𝐶‘𝑖) ∈ ran (𝑇‘(𝐶‘(𝑖 − 1))))) |
9 | 8 | simp1bi 1069 |
. . . . . . 7
⊢ (𝐶 ∈ dom 𝑆 → 𝐶 ∈ (Word 𝑊 ∖ {∅})) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (Word 𝑊 ∖ {∅})) |
11 | 10 | eldifad 3552 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Word 𝑊) |
12 | | efgredlem.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ dom 𝑆) |
13 | 2, 3, 4, 5, 6, 7 | efgsdm 17966 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1))))) |
14 | 13 | simp1bi 1069 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) |
16 | 15 | eldifad 3552 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Word 𝑊) |
17 | | wrdf 13165 |
. . . . . . . 8
⊢ (𝐴 ∈ Word 𝑊 → 𝐴:(0..^(#‘𝐴))⟶𝑊) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴:(0..^(#‘𝐴))⟶𝑊) |
19 | | fzossfz 12357 |
. . . . . . . . 9
⊢
(0..^((#‘𝐴)
− 1)) ⊆ (0...((#‘𝐴) − 1)) |
20 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑊 → (#‘𝐴) ∈
ℕ0) |
21 | 16, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐴) ∈
ℕ0) |
22 | 21 | nn0zd 11356 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐴) ∈ ℤ) |
23 | | fzoval 12340 |
. . . . . . . . . 10
⊢
((#‘𝐴) ∈
ℤ → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1))) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1))) |
25 | 19, 24 | syl5sseqr 3617 |
. . . . . . . 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 17976 |
. . . . . . . . . . 11
⊢ (𝜑 → (((#‘𝐴) − 1) ∈ ℕ
∧ ((#‘𝐵) −
1) ∈ ℕ)) |
32 | 31 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐴) − 1) ∈
ℕ) |
33 | | fzo0end 12426 |
. . . . . . . . . 10
⊢
(((#‘𝐴)
− 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈
(0..^((#‘𝐴) −
1))) |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈
(0..^((#‘𝐴) −
1))) |
35 | 26, 34 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (0..^((#‘𝐴) − 1))) |
36 | 25, 35 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (0..^(#‘𝐴))) |
37 | 18, 36 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊) |
38 | 37 | s1cld 13236 |
. . . . 5
⊢ (𝜑 → 〈“(𝐴‘𝐾)”〉 ∈ Word 𝑊) |
39 | | eldifsn 4260 |
. . . . . . . 8
⊢ (𝐶 ∈ (Word 𝑊 ∖ {∅}) ↔ (𝐶 ∈ Word 𝑊 ∧ 𝐶 ≠ ∅)) |
40 | | lennncl 13180 |
. . . . . . . 8
⊢ ((𝐶 ∈ Word 𝑊 ∧ 𝐶 ≠ ∅) → (#‘𝐶) ∈
ℕ) |
41 | 39, 40 | sylbi 206 |
. . . . . . 7
⊢ (𝐶 ∈ (Word 𝑊 ∖ {∅}) → (#‘𝐶) ∈
ℕ) |
42 | 10, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝐶) ∈ ℕ) |
43 | | lbfzo0 12375 |
. . . . . 6
⊢ (0 ∈
(0..^(#‘𝐶)) ↔
(#‘𝐶) ∈
ℕ) |
44 | 42, 43 | sylibr 223 |
. . . . 5
⊢ (𝜑 → 0 ∈
(0..^(#‘𝐶))) |
45 | | ccatval1 13214 |
. . . . 5
⊢ ((𝐶 ∈ Word 𝑊 ∧ 〈“(𝐴‘𝐾)”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(#‘𝐶))) → ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0) = (𝐶‘0)) |
46 | 11, 38, 44, 45 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0) = (𝐶‘0)) |
47 | 2, 3, 4, 5, 6, 7 | efgsdm 17966 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1))))) |
48 | 47 | simp1bi 1069 |
. . . . . . . . . 10
⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) |
49 | 28, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) |
50 | 49 | eldifad 3552 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Word 𝑊) |
51 | | wrdf 13165 |
. . . . . . . 8
⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(#‘𝐵))⟶𝑊) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵:(0..^(#‘𝐵))⟶𝑊) |
53 | | fzossfz 12357 |
. . . . . . . . 9
⊢
(0..^((#‘𝐵)
− 1)) ⊆ (0...((#‘𝐵) − 1)) |
54 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Word 𝑊 → (#‘𝐵) ∈
ℕ0) |
55 | 50, 54 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐵) ∈
ℕ0) |
56 | 55 | nn0zd 11356 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐵) ∈ ℤ) |
57 | | fzoval 12340 |
. . . . . . . . . 10
⊢
((#‘𝐵) ∈
ℤ → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1))) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1))) |
59 | 53, 58 | syl5sseqr 3617 |
. . . . . . . 8
⊢ (𝜑 → (0..^((#‘𝐵) − 1)) ⊆
(0..^(#‘𝐵))) |
60 | | efgredlemb.l |
. . . . . . . . 9
⊢ 𝐿 = (((#‘𝐵) − 1) − 1) |
61 | 31 | simprd 478 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐵) − 1) ∈
ℕ) |
62 | | fzo0end 12426 |
. . . . . . . . . 10
⊢
(((#‘𝐵)
− 1) ∈ ℕ → (((#‘𝐵) − 1) − 1) ∈
(0..^((#‘𝐵) −
1))) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈
(0..^((#‘𝐵) −
1))) |
64 | 60, 63 | syl5eqel 2692 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (0..^((#‘𝐵) − 1))) |
65 | 59, 64 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (0..^(#‘𝐵))) |
66 | 52, 65 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊) |
67 | 66 | s1cld 13236 |
. . . . 5
⊢ (𝜑 → 〈“(𝐵‘𝐿)”〉 ∈ Word 𝑊) |
68 | | ccatval1 13214 |
. . . . 5
⊢ ((𝐶 ∈ Word 𝑊 ∧ 〈“(𝐵‘𝐿)”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(#‘𝐶))) → ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0) = (𝐶‘0)) |
69 | 11, 67, 44, 68 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0) = (𝐶‘0)) |
70 | 46, 69 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)) |
71 | | fviss 6166 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
72 | 2, 71 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
73 | 72, 37 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 ×
2𝑜)) |
74 | | lencl 13179 |
. . . . . . . 8
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝐴‘𝐾)) ∈
ℕ0) |
75 | 73, 74 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
ℕ0) |
76 | 75 | nn0red 11229 |
. . . . . 6
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈ ℝ) |
77 | | 2rp 11713 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
78 | | ltaddrp 11743 |
. . . . . 6
⊢
(((#‘(𝐴‘𝐾)) ∈ ℝ ∧ 2 ∈
ℝ+) → (#‘(𝐴‘𝐾)) < ((#‘(𝐴‘𝐾)) + 2)) |
79 | 76, 77, 78 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (#‘(𝐴‘𝐾)) < ((#‘(𝐴‘𝐾)) + 2)) |
80 | 21 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐴) ∈ ℝ) |
81 | 80 | lem1d 10836 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐴) − 1) ≤ (#‘𝐴)) |
82 | | fznn 12278 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℤ → (((#‘𝐴) − 1) ∈ (1...(#‘𝐴)) ↔ (((#‘𝐴) − 1) ∈ ℕ
∧ ((#‘𝐴) −
1) ≤ (#‘𝐴)))) |
83 | 22, 82 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((#‘𝐴) − 1) ∈
(1...(#‘𝐴)) ↔
(((#‘𝐴) − 1)
∈ ℕ ∧ ((#‘𝐴) − 1) ≤ (#‘𝐴)))) |
84 | 32, 81, 83 | mpbir2and 959 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝐴) − 1) ∈
(1...(#‘𝐴))) |
85 | 2, 3, 4, 5, 6, 7 | efgsres 17974 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ (1...(#‘𝐴))) → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆) |
86 | 12, 84, 85 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆) |
87 | 2, 3, 4, 5, 6, 7 | efgsval 17967 |
. . . . . . . 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 | | 1eluzge0 11608 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
(ℤ≥‘0) |
90 | | fzss1 12251 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
(ℤ≥‘0) → (1...(#‘𝐴)) ⊆ (0...(#‘𝐴))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(1...(#‘𝐴))
⊆ (0...(#‘𝐴)) |
92 | 91, 84 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((#‘𝐴) − 1) ∈
(0...(#‘𝐴))) |
93 | | swrd0val 13273 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (𝐴 substr 〈0, ((#‘𝐴) − 1)〉) = (𝐴 ↾ (0..^((#‘𝐴) − 1)))) |
94 | 16, 92, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 substr 〈0, ((#‘𝐴) − 1)〉) = (𝐴 ↾ (0..^((#‘𝐴) − 1)))) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐴 substr 〈0, ((#‘𝐴) − 1)〉)) =
(#‘(𝐴 ↾
(0..^((#‘𝐴) −
1))))) |
96 | | swrd0len 13274 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑊 ∧ ((#‘𝐴) − 1) ∈ (0...(#‘𝐴))) → (#‘(𝐴 substr 〈0, ((#‘𝐴) − 1)〉)) =
((#‘𝐴) −
1)) |
97 | 16, 92, 96 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐴 substr 〈0, ((#‘𝐴) − 1)〉)) =
((#‘𝐴) −
1)) |
98 | 95, 97 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) =
((#‘𝐴) −
1)) |
99 | 98 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1) =
(((#‘𝐴) − 1)
− 1)) |
100 | 99, 26 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝜑 → ((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1) =
𝐾) |
101 | 100 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘((#‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) − 1)) =
((𝐴 ↾
(0..^((#‘𝐴) −
1)))‘𝐾)) |
102 | | fvres 6117 |
. . . . . . . 8
⊢ (𝐾 ∈ (0..^((#‘𝐴) − 1)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘𝐾) = (𝐴‘𝐾)) |
103 | 35, 102 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘𝐾) = (𝐴‘𝐾)) |
104 | 88, 101, 103 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝐴‘𝐾)) |
105 | 104 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) = (#‘(𝐴‘𝐾))) |
106 | 2, 3, 4, 5, 6, 7 | efgsdmi 17968 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom 𝑆 ∧ ((#‘𝐴) − 1) ∈ ℕ) → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))) |
107 | 12, 32, 106 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1)))) |
108 | 26 | fveq2i 6106 |
. . . . . . . . 9
⊢ (𝐴‘𝐾) = (𝐴‘(((#‘𝐴) − 1) − 1)) |
109 | 108 | fveq2i 6106 |
. . . . . . . 8
⊢ (𝑇‘(𝐴‘𝐾)) = (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) |
110 | 109 | rneqi 5273 |
. . . . . . 7
⊢ ran
(𝑇‘(𝐴‘𝐾)) = ran (𝑇‘(𝐴‘(((#‘𝐴) − 1) − 1))) |
111 | 107, 110 | syl6eleqr 2699 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘𝐾))) |
112 | 2, 3, 4, 5 | efgtlen 17962 |
. . . . . 6
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐴‘𝐾))) → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘𝐾)) + 2)) |
113 | 37, 111, 112 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (#‘(𝑆‘𝐴)) = ((#‘(𝐴‘𝐾)) + 2)) |
114 | 79, 105, 113 | 3brtr4d 4615 |
. . . 4
⊢ (𝜑 → (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴))) |
115 | | efgredlemb.p |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) |
116 | | efgredlemb.q |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) |
117 | | efgredlemb.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ (𝐼 ×
2𝑜)) |
118 | | efgredlemb.v |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ (𝐼 ×
2𝑜)) |
119 | | efgredlemb.6 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) |
120 | | efgredlemb.7 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) |
121 | | efgredlemb.8 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) |
122 | | efgredlemd.9 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) |
123 | | efgredlemd.sc |
. . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝐶) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
124 | 2, 3, 4, 5, 6, 7, 27, 12, 28, 29, 30, 26, 60, 115, 116, 117, 118, 119, 120, 121, 122, 1, 123 | efgredleme 17979 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶)) ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶)))) |
125 | 124 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) |
126 | 2, 3, 4, 5, 6, 7 | efgsp1 17973 |
. . . . . . 7
⊢ ((𝐶 ∈ dom 𝑆 ∧ (𝐴‘𝐾) ∈ ran (𝑇‘(𝑆‘𝐶))) → (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) |
127 | 1, 125, 126 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) |
128 | 2, 3, 4, 5, 6, 7 | efgsval2 17969 |
. . . . . 6
⊢ ((𝐶 ∈ Word 𝑊 ∧ (𝐴‘𝐾) ∈ 𝑊 ∧ (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) → (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) = (𝐴‘𝐾)) |
129 | 11, 37, 127, 128 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) = (𝐴‘𝐾)) |
130 | 104, 129 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉))) |
131 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) |
132 | 131 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (#‘(𝑆‘𝑎)) = (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))))) |
133 | 132 | breq1d 4593 |
. . . . . . 7
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) ↔ (#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)))) |
134 | 131 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏))) |
135 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (𝑎‘0) = ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0)) |
136 | 135 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0))) |
137 | 134, 136 | imbi12d 333 |
. . . . . . 7
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)))) |
138 | 133, 137 | imbi12d 333 |
. . . . . 6
⊢ (𝑎 = (𝐴 ↾ (0..^((#‘𝐴) − 1))) → (((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0))))) |
139 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (𝑆‘𝑏) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉))) |
140 | 139 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)))) |
141 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (𝑏‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)) |
142 | 141 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0) ↔ ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) =
((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0))) |
143 | 140, 142 | imbi12d 333 |
. . . . . . 7
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)))) |
144 | 143 | imbi2d 329 |
. . . . . 6
⊢ (𝑏 = (𝐶 ++ 〈“(𝐴‘𝐾)”〉) → (((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘𝑏) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝑏‘0))) ↔
((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) <
(#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0))))) |
145 | 138, 144 | rspc2va 3294 |
. . . . 5
⊢ ((((𝐴 ↾ (0..^((#‘𝐴) − 1))) ∈ dom 𝑆 ∧ (𝐶 ++ 〈“(𝐴‘𝐾)”〉) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)))) |
146 | 86, 127, 27, 145 | syl21anc 1317 |
. . . 4
⊢ (𝜑 → ((#‘(𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐴 ↾ (0..^((#‘𝐴) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐴‘𝐾)”〉)) → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)))) |
147 | 114, 130,
146 | mp2d 47 |
. . 3
⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐶 ++ 〈“(𝐴‘𝐾)”〉)‘0)) |
148 | 72, 66 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 ×
2𝑜)) |
149 | | lencl 13179 |
. . . . . . . 8
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝐵‘𝐿)) ∈
ℕ0) |
150 | 148, 149 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
ℕ0) |
151 | 150 | nn0red 11229 |
. . . . . 6
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈ ℝ) |
152 | | ltaddrp 11743 |
. . . . . 6
⊢
(((#‘(𝐵‘𝐿)) ∈ ℝ ∧ 2 ∈
ℝ+) → (#‘(𝐵‘𝐿)) < ((#‘(𝐵‘𝐿)) + 2)) |
153 | 151, 77, 152 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (#‘(𝐵‘𝐿)) < ((#‘(𝐵‘𝐿)) + 2)) |
154 | 55 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐵) ∈ ℝ) |
155 | 154 | lem1d 10836 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐵) − 1) ≤ (#‘𝐵)) |
156 | | fznn 12278 |
. . . . . . . . . . 11
⊢
((#‘𝐵) ∈
ℤ → (((#‘𝐵) − 1) ∈ (1...(#‘𝐵)) ↔ (((#‘𝐵) − 1) ∈ ℕ
∧ ((#‘𝐵) −
1) ≤ (#‘𝐵)))) |
157 | 56, 156 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((#‘𝐵) − 1) ∈
(1...(#‘𝐵)) ↔
(((#‘𝐵) − 1)
∈ ℕ ∧ ((#‘𝐵) − 1) ≤ (#‘𝐵)))) |
158 | 61, 155, 157 | mpbir2and 959 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝐵) − 1) ∈
(1...(#‘𝐵))) |
159 | 2, 3, 4, 5, 6, 7 | efgsres 17974 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ (1...(#‘𝐵))) → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆) |
160 | 28, 158, 159 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆) |
161 | 2, 3, 4, 5, 6, 7 | efgsval 17967 |
. . . . . . . 8
⊢ ((𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆 → (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) −
1))) |
162 | 160, 161 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) −
1))) |
163 | | fzss1 12251 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
(ℤ≥‘0) → (1...(#‘𝐵)) ⊆ (0...(#‘𝐵))) |
164 | 89, 163 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(1...(#‘𝐵))
⊆ (0...(#‘𝐵)) |
165 | 164, 158 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((#‘𝐵) − 1) ∈
(0...(#‘𝐵))) |
166 | | swrd0val 13273 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (𝐵 substr 〈0, ((#‘𝐵) − 1)〉) = (𝐵 ↾ (0..^((#‘𝐵) − 1)))) |
167 | 50, 165, 166 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 substr 〈0, ((#‘𝐵) − 1)〉) = (𝐵 ↾ (0..^((#‘𝐵) − 1)))) |
168 | 167 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐵 substr 〈0, ((#‘𝐵) − 1)〉)) =
(#‘(𝐵 ↾
(0..^((#‘𝐵) −
1))))) |
169 | | swrd0len 13274 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ Word 𝑊 ∧ ((#‘𝐵) − 1) ∈ (0...(#‘𝐵))) → (#‘(𝐵 substr 〈0, ((#‘𝐵) − 1)〉)) =
((#‘𝐵) −
1)) |
170 | 50, 165, 169 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐵 substr 〈0, ((#‘𝐵) − 1)〉)) =
((#‘𝐵) −
1)) |
171 | 168, 170 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) =
((#‘𝐵) −
1)) |
172 | 171 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1) =
(((#‘𝐵) − 1)
− 1)) |
173 | 172, 60 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝜑 → ((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1) =
𝐿) |
174 | 173 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘((#‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) − 1)) =
((𝐵 ↾
(0..^((#‘𝐵) −
1)))‘𝐿)) |
175 | | fvres 6117 |
. . . . . . . 8
⊢ (𝐿 ∈ (0..^((#‘𝐵) − 1)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘𝐿) = (𝐵‘𝐿)) |
176 | 64, 175 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘𝐿) = (𝐵‘𝐿)) |
177 | 162, 174,
176 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝐵‘𝐿)) |
178 | 177 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) = (#‘(𝐵‘𝐿))) |
179 | 2, 3, 4, 5, 6, 7 | efgsdmi 17968 |
. . . . . . . . 9
⊢ ((𝐵 ∈ dom 𝑆 ∧ ((#‘𝐵) − 1) ∈ ℕ) → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))) |
180 | 28, 61, 179 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑆‘𝐵) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))) |
181 | 29, 180 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1)))) |
182 | 60 | fveq2i 6106 |
. . . . . . . . 9
⊢ (𝐵‘𝐿) = (𝐵‘(((#‘𝐵) − 1) − 1)) |
183 | 182 | fveq2i 6106 |
. . . . . . . 8
⊢ (𝑇‘(𝐵‘𝐿)) = (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) |
184 | 183 | rneqi 5273 |
. . . . . . 7
⊢ ran
(𝑇‘(𝐵‘𝐿)) = ran (𝑇‘(𝐵‘(((#‘𝐵) − 1) − 1))) |
185 | 181, 184 | syl6eleqr 2699 |
. . . . . 6
⊢ (𝜑 → (𝑆‘𝐴) ∈ ran (𝑇‘(𝐵‘𝐿))) |
186 | 2, 3, 4, 5 | efgtlen 17962 |
. . . . . 6
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑆‘𝐴) ∈ ran (𝑇‘(𝐵‘𝐿))) → (#‘(𝑆‘𝐴)) = ((#‘(𝐵‘𝐿)) + 2)) |
187 | 66, 185, 186 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (#‘(𝑆‘𝐴)) = ((#‘(𝐵‘𝐿)) + 2)) |
188 | 153, 178,
187 | 3brtr4d 4615 |
. . . 4
⊢ (𝜑 → (#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) < (#‘(𝑆‘𝐴))) |
189 | 124 | simprd 478 |
. . . . . . 7
⊢ (𝜑 → (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) |
190 | 2, 3, 4, 5, 6, 7 | efgsp1 17973 |
. . . . . . 7
⊢ ((𝐶 ∈ dom 𝑆 ∧ (𝐵‘𝐿) ∈ ran (𝑇‘(𝑆‘𝐶))) → (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) |
191 | 1, 189, 190 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) |
192 | 2, 3, 4, 5, 6, 7 | efgsval2 17969 |
. . . . . 6
⊢ ((𝐶 ∈ Word 𝑊 ∧ (𝐵‘𝐿) ∈ 𝑊 ∧ (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) → (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) = (𝐵‘𝐿)) |
193 | 11, 66, 191, 192 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) = (𝐵‘𝐿)) |
194 | 177, 193 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉))) |
195 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑆‘𝑎) = (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) |
196 | 195 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (#‘(𝑆‘𝑎)) = (#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))))) |
197 | 196 | breq1d 4593 |
. . . . . . 7
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → ((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) ↔ (#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) < (#‘(𝑆‘𝐴)))) |
198 | 195 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘𝑏))) |
199 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (𝑎‘0) = ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0)) |
200 | 199 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → ((𝑎‘0) = (𝑏‘0) ↔ ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝑏‘0))) |
201 | 198, 200 | imbi12d 333 |
. . . . . . 7
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝑏‘0)))) |
202 | 197, 201 | imbi12d 333 |
. . . . . 6
⊢ (𝑎 = (𝐵 ↾ (0..^((#‘𝐵) − 1))) → (((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝑏‘0))))) |
203 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (𝑆‘𝑏) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉))) |
204 | 203 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘𝑏) ↔ (𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)))) |
205 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (𝑏‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)) |
206 | 205 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝑏‘0) ↔ ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) =
((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0))) |
207 | 204, 206 | imbi12d 333 |
. . . . . . 7
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝑏‘0)) ↔ ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)))) |
208 | 207 | imbi2d 329 |
. . . . . 6
⊢ (𝑏 = (𝐶 ++ 〈“(𝐵‘𝐿)”〉) → (((#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘𝑏) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝑏‘0))) ↔
((#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) <
(#‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0))))) |
209 | 202, 208 | rspc2va 3294 |
. . . . 5
⊢ ((((𝐵 ↾ (0..^((#‘𝐵) − 1))) ∈ dom 𝑆 ∧ (𝐶 ++ 〈“(𝐵‘𝐿)”〉) ∈ dom 𝑆) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) → ((#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)))) |
210 | 160, 191,
27, 209 | syl21anc 1317 |
. . . 4
⊢ (𝜑 → ((#‘(𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1))))) < (#‘(𝑆‘𝐴)) → ((𝑆‘(𝐵 ↾ (0..^((#‘𝐵) − 1)))) = (𝑆‘(𝐶 ++ 〈“(𝐵‘𝐿)”〉)) → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)))) |
211 | 188, 194,
210 | mp2d 47 |
. . 3
⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = ((𝐶 ++ 〈“(𝐵‘𝐿)”〉)‘0)) |
212 | 70, 147, 211 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = ((𝐵 ↾ (0..^((#‘𝐵) −
1)))‘0)) |
213 | | lbfzo0 12375 |
. . . 4
⊢ (0 ∈
(0..^((#‘𝐴) −
1)) ↔ ((#‘𝐴)
− 1) ∈ ℕ) |
214 | 32, 213 | sylibr 223 |
. . 3
⊢ (𝜑 → 0 ∈
(0..^((#‘𝐴) −
1))) |
215 | | fvres 6117 |
. . 3
⊢ (0 ∈
(0..^((#‘𝐴) −
1)) → ((𝐴 ↾
(0..^((#‘𝐴) −
1)))‘0) = (𝐴‘0)) |
216 | 214, 215 | syl 17 |
. 2
⊢ (𝜑 → ((𝐴 ↾ (0..^((#‘𝐴) − 1)))‘0) = (𝐴‘0)) |
217 | | lbfzo0 12375 |
. . . 4
⊢ (0 ∈
(0..^((#‘𝐵) −
1)) ↔ ((#‘𝐵)
− 1) ∈ ℕ) |
218 | 61, 217 | sylibr 223 |
. . 3
⊢ (𝜑 → 0 ∈
(0..^((#‘𝐵) −
1))) |
219 | | fvres 6117 |
. . 3
⊢ (0 ∈
(0..^((#‘𝐵) −
1)) → ((𝐵 ↾
(0..^((#‘𝐵) −
1)))‘0) = (𝐵‘0)) |
220 | 218, 219 | syl 17 |
. 2
⊢ (𝜑 → ((𝐵 ↾ (0..^((#‘𝐵) − 1)))‘0) = (𝐵‘0)) |
221 | 212, 216,
220 | 3eqtr3d 2652 |
1
⊢ (𝜑 → (𝐴‘0) = (𝐵‘0)) |