Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . 8
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | efgval.r |
. . . . . . . 8
⊢ ∼ = (
~FG ‘𝐼) |
3 | | efgval2.m |
. . . . . . . 8
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
4 | | efgval2.t |
. . . . . . . 8
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
5 | | efgred.d |
. . . . . . . 8
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
6 | | efgred.s |
. . . . . . . 8
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. . . . . . 7
⊢ (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) |
8 | 7 | simp1bi 1076 |
. . . . . 6
⊢ (𝐹 ∈ dom 𝑆 → 𝐹 ∈ (Word 𝑊 ∖ {∅})) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 𝐹 ∈ (Word 𝑊 ∖ {∅})) |
10 | 9 | eldifad 3586 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 𝐹 ∈ Word 𝑊) |
11 | 1, 2, 3, 4, 5, 6 | efgsf 18142 |
. . . . . . . . . . . 12
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 |
12 | 11 | fdmi 6052 |
. . . . . . . . . . . . 13
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} |
13 | 12 | feq2i 6037 |
. . . . . . . . . . . 12
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) |
14 | 11, 13 | mpbir 221 |
. . . . . . . . . . 11
⊢ 𝑆:dom 𝑆⟶𝑊 |
15 | 14 | ffvelrni 6358 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) ∈ 𝑊) |
16 | 15 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝑆‘𝐹) ∈ 𝑊) |
17 | 1, 2, 3, 4 | efgtf 18135 |
. . . . . . . . 9
⊢ ((𝑆‘𝐹) ∈ 𝑊 → ((𝑇‘(𝑆‘𝐹)) = (𝑎 ∈ (0...(#‘(𝑆‘𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦
((𝑆‘𝐹) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐹)):((0...(#‘(𝑆‘𝐹))) × (𝐼 ×
2𝑜))⟶𝑊)) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝑇‘(𝑆‘𝐹)) = (𝑎 ∈ (0...(#‘(𝑆‘𝐹))), 𝑖 ∈ (𝐼 × 2𝑜) ↦
((𝑆‘𝐹) splice 〈𝑎, 𝑎, 〈“𝑖(𝑀‘𝑖)”〉〉)) ∧ (𝑇‘(𝑆‘𝐹)):((0...(#‘(𝑆‘𝐹))) × (𝐼 ×
2𝑜))⟶𝑊)) |
19 | 18 | simprd 479 |
. . . . . . 7
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝑇‘(𝑆‘𝐹)):((0...(#‘(𝑆‘𝐹))) × (𝐼 ×
2𝑜))⟶𝑊) |
20 | | frn 6053 |
. . . . . . 7
⊢ ((𝑇‘(𝑆‘𝐹)):((0...(#‘(𝑆‘𝐹))) × (𝐼 ×
2𝑜))⟶𝑊 → ran (𝑇‘(𝑆‘𝐹)) ⊆ 𝑊) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ran (𝑇‘(𝑆‘𝐹)) ⊆ 𝑊) |
22 | | simpr 477 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) |
23 | 21, 22 | sseldd 3604 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 𝐴 ∈ 𝑊) |
24 | 23 | s1cld 13383 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 〈“𝐴”〉 ∈ Word 𝑊) |
25 | | ccatcl 13359 |
. . . 4
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊) → (𝐹 ++ 〈“𝐴”〉) ∈ Word 𝑊) |
26 | 10, 24, 25 | syl2anc 693 |
. . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹 ++ 〈“𝐴”〉) ∈ Word 𝑊) |
27 | | ccatlen 13360 |
. . . . . . 7
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊) → (#‘(𝐹 ++ 〈“𝐴”〉)) = ((#‘𝐹) + (#‘〈“𝐴”〉))) |
28 | 10, 24, 27 | syl2anc 693 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘(𝐹 ++ 〈“𝐴”〉)) = ((#‘𝐹) + (#‘〈“𝐴”〉))) |
29 | | s1len 13385 |
. . . . . . 7
⊢
(#‘〈“𝐴”〉) = 1 |
30 | 29 | oveq2i 6661 |
. . . . . 6
⊢
((#‘𝐹) +
(#‘〈“𝐴”〉)) = ((#‘𝐹) + 1) |
31 | 28, 30 | syl6eq 2672 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘(𝐹 ++ 〈“𝐴”〉)) = ((#‘𝐹) + 1)) |
32 | | lencl 13324 |
. . . . . 6
⊢ (𝐹 ∈ Word 𝑊 → (#‘𝐹) ∈
ℕ0) |
33 | | nn0p1nn 11332 |
. . . . . 6
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐹) + 1) ∈ ℕ) |
34 | 10, 32, 33 | 3syl 18 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((#‘𝐹) + 1) ∈ ℕ) |
35 | 31, 34 | eqeltrd 2701 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘(𝐹 ++ 〈“𝐴”〉)) ∈
ℕ) |
36 | | wrdfin 13323 |
. . . . 5
⊢ ((𝐹 ++ 〈“𝐴”〉) ∈ Word 𝑊 → (𝐹 ++ 〈“𝐴”〉) ∈ Fin) |
37 | | hashnncl 13157 |
. . . . 5
⊢ ((𝐹 ++ 〈“𝐴”〉) ∈ Fin →
((#‘(𝐹 ++
〈“𝐴”〉)) ∈ ℕ ↔ (𝐹 ++ 〈“𝐴”〉) ≠
∅)) |
38 | 26, 36, 37 | 3syl 18 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((#‘(𝐹 ++ 〈“𝐴”〉)) ∈ ℕ ↔ (𝐹 ++ 〈“𝐴”〉) ≠
∅)) |
39 | 35, 38 | mpbid 222 |
. . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹 ++ 〈“𝐴”〉) ≠
∅) |
40 | | eldifsn 4317 |
. . 3
⊢ ((𝐹 ++ 〈“𝐴”〉) ∈ (Word
𝑊 ∖ {∅}) ↔
((𝐹 ++ 〈“𝐴”〉) ∈ Word 𝑊 ∧ (𝐹 ++ 〈“𝐴”〉) ≠
∅)) |
41 | 26, 39, 40 | sylanbrc 698 |
. 2
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹 ++ 〈“𝐴”〉) ∈ (Word 𝑊 ∖
{∅})) |
42 | | eldifsni 4320 |
. . . . . . 7
⊢ (𝐹 ∈ (Word 𝑊 ∖ {∅}) → 𝐹 ≠ ∅) |
43 | 9, 42 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 𝐹 ≠ ∅) |
44 | | wrdfin 13323 |
. . . . . . 7
⊢ (𝐹 ∈ Word 𝑊 → 𝐹 ∈ Fin) |
45 | | hashnncl 13157 |
. . . . . . 7
⊢ (𝐹 ∈ Fin →
((#‘𝐹) ∈ ℕ
↔ 𝐹 ≠
∅)) |
46 | 10, 44, 45 | 3syl 18 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((#‘𝐹) ∈ ℕ ↔ 𝐹 ≠ ∅)) |
47 | 43, 46 | mpbird 247 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘𝐹) ∈ ℕ) |
48 | | lbfzo0 12507 |
. . . . 5
⊢ (0 ∈
(0..^(#‘𝐹)) ↔
(#‘𝐹) ∈
ℕ) |
49 | 47, 48 | sylibr 224 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 0 ∈ (0..^(#‘𝐹))) |
50 | | ccatval1 13361 |
. . . 4
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 0 ∈ (0..^(#‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘0) = (𝐹‘0)) |
51 | 10, 24, 49, 50 | syl3anc 1326 |
. . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘0) = (𝐹‘0)) |
52 | 7 | simp2bi 1077 |
. . . 4
⊢ (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∈ 𝐷) |
53 | 52 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹‘0) ∈ 𝐷) |
54 | 51, 53 | eqeltrd 2701 |
. 2
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘0) ∈ 𝐷) |
55 | 7 | simp3bi 1078 |
. . . . . 6
⊢ (𝐹 ∈ dom 𝑆 → ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))) |
56 | 55 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))) |
57 | | fzo0ss1 12498 |
. . . . . . . . . . 11
⊢
(1..^(#‘𝐹))
⊆ (0..^(#‘𝐹)) |
58 | 57 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → 𝑖 ∈ (0..^(#‘𝐹))) |
59 | | ccatval1 13361 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘𝑖) = (𝐹‘𝑖)) |
60 | 58, 59 | syl3an3 1361 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 𝑖 ∈ (1..^(#‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘𝑖) = (𝐹‘𝑖)) |
61 | | elfzoel2 12469 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈
ℤ) |
62 | | peano2zm 11420 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℤ → ((#‘𝐹)
− 1) ∈ ℤ) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → ((#‘𝐹) − 1) ∈
ℤ) |
64 | 61 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈
ℝ) |
65 | 64 | lem1d 10957 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → ((#‘𝐹) − 1) ≤ (#‘𝐹)) |
66 | | eluz2 11693 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1)) ↔ (((#‘𝐹) − 1) ∈ ℤ
∧ (#‘𝐹) ∈
ℤ ∧ ((#‘𝐹)
− 1) ≤ (#‘𝐹))) |
67 | 63, 61, 65, 66 | syl3anbrc 1246 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1))) |
68 | | fzoss2 12496 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) ∈
(ℤ≥‘((#‘𝐹) − 1)) → (0..^((#‘𝐹) − 1)) ⊆
(0..^(#‘𝐹))) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (0..^((#‘𝐹) − 1)) ⊆
(0..^(#‘𝐹))) |
70 | | elfzoelz 12470 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → 𝑖 ∈ ℤ) |
71 | | elfzom1b 12567 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ ℤ ∧
(#‘𝐹) ∈ ℤ)
→ (𝑖 ∈
(1..^(#‘𝐹)) ↔
(𝑖 − 1) ∈
(0..^((#‘𝐹) −
1)))) |
72 | 70, 61, 71 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (𝑖 ∈ (1..^(#‘𝐹)) ↔ (𝑖 − 1) ∈ (0..^((#‘𝐹) − 1)))) |
73 | 72 | ibi 256 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (𝑖 − 1) ∈ (0..^((#‘𝐹) − 1))) |
74 | 69, 73 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1..^(#‘𝐹)) → (𝑖 − 1) ∈ (0..^(#‘𝐹))) |
75 | | ccatval1 13361 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ (𝑖 − 1) ∈ (0..^(#‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1))) |
76 | 74, 75 | syl3an3 1361 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 𝑖 ∈ (1..^(#‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1))) |
77 | 76 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 𝑖 ∈ (1..^(#‘𝐹))) → (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) = (𝑇‘(𝐹‘(𝑖 − 1)))) |
78 | 77 | rneqd 5353 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 𝑖 ∈ (1..^(#‘𝐹))) → ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) = ran (𝑇‘(𝐹‘(𝑖 − 1)))) |
79 | 60, 78 | eleq12d 2695 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 𝑖 ∈ (1..^(#‘𝐹))) → (((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ (𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) |
80 | 79 | 3expa 1265 |
. . . . . . 7
⊢ (((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊) ∧ 𝑖 ∈ (1..^(#‘𝐹))) → (((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ (𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) |
81 | 80 | ralbidva 2985 |
. . . . . 6
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊) → (∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) |
82 | 10, 24, 81 | syl2anc 693 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^(#‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) |
83 | 56, 82 | mpbird 247 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)))) |
84 | 10, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘𝐹) ∈
ℕ0) |
85 | 84 | nn0cnd 11353 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘𝐹) ∈ ℂ) |
86 | 85 | addid2d 10237 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (0 + (#‘𝐹)) = (#‘𝐹)) |
87 | 86 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘(0 + (#‘𝐹))) = ((𝐹 ++ 〈“𝐴”〉)‘(#‘𝐹))) |
88 | | 1nn 11031 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
89 | 29, 88 | eqeltri 2697 |
. . . . . . . . . 10
⊢
(#‘〈“𝐴”〉) ∈
ℕ |
90 | 89 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘〈“𝐴”〉) ∈
ℕ) |
91 | | lbfzo0 12507 |
. . . . . . . . 9
⊢ (0 ∈
(0..^(#‘〈“𝐴”〉)) ↔
(#‘〈“𝐴”〉) ∈
ℕ) |
92 | 90, 91 | sylibr 224 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → 0 ∈
(0..^(#‘〈“𝐴”〉))) |
93 | | ccatval3 13363 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ 0 ∈
(0..^(#‘〈“𝐴”〉))) → ((𝐹 ++ 〈“𝐴”〉)‘(0 + (#‘𝐹))) = (〈“𝐴”〉‘0)) |
94 | 10, 24, 92, 93 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘(0 + (#‘𝐹))) = (〈“𝐴”〉‘0)) |
95 | 87, 94 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘(#‘𝐹)) = (〈“𝐴”〉‘0)) |
96 | | s1fv 13390 |
. . . . . . . 8
⊢ (𝐴 ∈ ran (𝑇‘(𝑆‘𝐹)) → (〈“𝐴”〉‘0) = 𝐴) |
97 | 96 | adantl 482 |
. . . . . . 7
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (〈“𝐴”〉‘0) = 𝐴) |
98 | | fzo0end 12560 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) ∈
ℕ → ((#‘𝐹)
− 1) ∈ (0..^(#‘𝐹))) |
99 | 47, 98 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) |
100 | | ccatval1 13361 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word 𝑊 ∧ 〈“𝐴”〉 ∈ Word 𝑊 ∧ ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)) = (𝐹‘((#‘𝐹) − 1))) |
101 | 10, 24, 99, 100 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)) = (𝐹‘((#‘𝐹) − 1))) |
102 | 1, 2, 3, 4, 5, 6 | efgsval 18144 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) = (𝐹‘((#‘𝐹) − 1))) |
103 | 102 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝑆‘𝐹) = (𝐹‘((#‘𝐹) − 1))) |
104 | 101, 103 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)) = (𝑆‘𝐹)) |
105 | 104 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1))) = (𝑇‘(𝑆‘𝐹))) |
106 | 105 | rneqd 5353 |
. . . . . . 7
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1))) = ran (𝑇‘(𝑆‘𝐹))) |
107 | 22, 97, 106 | 3eltr4d 2716 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (〈“𝐴”〉‘0) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)))) |
108 | 95, 107 | eqeltrd 2701 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ((𝐹 ++ 〈“𝐴”〉)‘(#‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)))) |
109 | | fvex 6201 |
. . . . . 6
⊢
(#‘𝐹) ∈
V |
110 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑖 = (#‘𝐹) → ((𝐹 ++ 〈“𝐴”〉)‘𝑖) = ((𝐹 ++ 〈“𝐴”〉)‘(#‘𝐹))) |
111 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑖 = (#‘𝐹) → (𝑖 − 1) = ((#‘𝐹) − 1)) |
112 | 111 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑖 = (#‘𝐹) → ((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)) = ((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1))) |
113 | 112 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑖 = (#‘𝐹) → (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) = (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)))) |
114 | 113 | rneqd 5353 |
. . . . . . 7
⊢ (𝑖 = (#‘𝐹) → ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) = ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)))) |
115 | 110, 114 | eleq12d 2695 |
. . . . . 6
⊢ (𝑖 = (#‘𝐹) → (((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ ((𝐹 ++ 〈“𝐴”〉)‘(#‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) −
1))))) |
116 | 109, 115 | ralsn 4222 |
. . . . 5
⊢
(∀𝑖 ∈
{(#‘𝐹)} ((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ ((𝐹 ++ 〈“𝐴”〉)‘(#‘𝐹)) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘((#‘𝐹) − 1)))) |
117 | 108, 116 | sylibr 224 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ∀𝑖 ∈ {(#‘𝐹)} ((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)))) |
118 | | ralunb 3794 |
. . . 4
⊢
(∀𝑖 ∈
((1..^(#‘𝐹)) ∪
{(#‘𝐹)})((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ (∀𝑖 ∈ (1..^(#‘𝐹))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ∧ ∀𝑖 ∈ {(#‘𝐹)} ((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))))) |
119 | 83, 117, 118 | sylanbrc 698 |
. . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ∀𝑖 ∈ ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)))) |
120 | 31 | oveq2d 6666 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (1..^(#‘(𝐹 ++ 〈“𝐴”〉))) = (1..^((#‘𝐹) + 1))) |
121 | | nnuz 11723 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
122 | 47, 121 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (#‘𝐹) ∈
(ℤ≥‘1)) |
123 | | fzosplitsn 12576 |
. . . . . 6
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → (1..^((#‘𝐹) + 1)) = ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})) |
124 | 122, 123 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (1..^((#‘𝐹) + 1)) = ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})) |
125 | 120, 124 | eqtrd 2656 |
. . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (1..^(#‘(𝐹 ++ 〈“𝐴”〉))) = ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})) |
126 | 125 | raleqdv 3144 |
. . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (∀𝑖 ∈ (1..^(#‘(𝐹 ++ 〈“𝐴”〉)))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))) ↔ ∀𝑖 ∈ ((1..^(#‘𝐹)) ∪ {(#‘𝐹)})((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))))) |
127 | 119, 126 | mpbird 247 |
. 2
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → ∀𝑖 ∈ (1..^(#‘(𝐹 ++ 〈“𝐴”〉)))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1)))) |
128 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. 2
⊢ ((𝐹 ++ 〈“𝐴”〉) ∈ dom 𝑆 ↔ ((𝐹 ++ 〈“𝐴”〉) ∈ (Word 𝑊 ∖ {∅}) ∧
((𝐹 ++ 〈“𝐴”〉)‘0) ∈
𝐷 ∧ ∀𝑖 ∈ (1..^(#‘(𝐹 ++ 〈“𝐴”〉)))((𝐹 ++ 〈“𝐴”〉)‘𝑖) ∈ ran (𝑇‘((𝐹 ++ 〈“𝐴”〉)‘(𝑖 − 1))))) |
129 | 41, 54, 127, 128 | syl3anbrc 1246 |
1
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝐴 ∈ ran (𝑇‘(𝑆‘𝐹))) → (𝐹 ++ 〈“𝐴”〉) ∈ dom 𝑆) |