| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | efgval.w | . . . . . . . . 9
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 2 |  | efgval.r | . . . . . . . . 9
⊢  ∼ = (
~FG ‘𝐼) | 
| 3 |  | efgval2.m | . . . . . . . . 9
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) | 
| 4 |  | efgval2.t | . . . . . . . . 9
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) | 
| 5 |  | efgred.d | . . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) | 
| 6 |  | efgred.s | . . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) | 
| 7 | 1, 2, 3, 4, 5, 6 | efgsdm 19749 | . . . . . . . 8
⊢ (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) | 
| 8 | 7 | simp1bi 1145 | . . . . . . 7
⊢ (𝐹 ∈ dom 𝑆 → 𝐹 ∈ (Word 𝑊 ∖ {∅})) | 
| 9 | 8 | adantr 480 | . . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → 𝐹 ∈ (Word 𝑊 ∖ {∅})) | 
| 10 | 9 | eldifad 3962 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → 𝐹 ∈ Word 𝑊) | 
| 11 |  | fz1ssfz0 13664 | . . . . . 6
⊢
(1...(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) | 
| 12 |  | simpr 484 | . . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ (1...(♯‘𝐹))) | 
| 13 | 11, 12 | sselid 3980 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ (0...(♯‘𝐹))) | 
| 14 |  | pfxres 14718 | . . . . 5
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁))) | 
| 15 | 10, 13, 14 | syl2anc 584 | . . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 prefix 𝑁) = (𝐹 ↾ (0..^𝑁))) | 
| 16 |  | pfxcl 14716 | . . . . 5
⊢ (𝐹 ∈ Word 𝑊 → (𝐹 prefix 𝑁) ∈ Word 𝑊) | 
| 17 | 10, 16 | syl 17 | . . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 prefix 𝑁) ∈ Word 𝑊) | 
| 18 | 15, 17 | eqeltrrd 2841 | . . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ∈ Word 𝑊) | 
| 19 |  | pfxlen 14722 | . . . . . . 7
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) = 𝑁) | 
| 20 | 10, 13, 19 | syl2anc 584 | . . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) = 𝑁) | 
| 21 |  | elfznn 13594 | . . . . . . 7
⊢ (𝑁 ∈
(1...(♯‘𝐹))
→ 𝑁 ∈
ℕ) | 
| 22 | 21 | adantl 481 | . . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℕ) | 
| 23 | 20, 22 | eqeltrd 2840 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) ∈ ℕ) | 
| 24 |  | wrdfin 14571 | . . . . . 6
⊢ ((𝐹 prefix 𝑁) ∈ Word 𝑊 → (𝐹 prefix 𝑁) ∈ Fin) | 
| 25 |  | hashnncl 14406 | . . . . . 6
⊢ ((𝐹 prefix 𝑁) ∈ Fin → ((♯‘(𝐹 prefix 𝑁)) ∈ ℕ ↔ (𝐹 prefix 𝑁) ≠ ∅)) | 
| 26 | 17, 24, 25 | 3syl 18 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) →
((♯‘(𝐹 prefix
𝑁)) ∈ ℕ ↔
(𝐹 prefix 𝑁) ≠ ∅)) | 
| 27 | 23, 26 | mpbid 232 | . . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 prefix 𝑁) ≠ ∅) | 
| 28 | 15, 27 | eqnetrrd 3008 | . . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ≠ ∅) | 
| 29 |  | eldifsn 4785 | . . 3
⊢ ((𝐹 ↾ (0..^𝑁)) ∈ (Word 𝑊 ∖ {∅}) ↔ ((𝐹 ↾ (0..^𝑁)) ∈ Word 𝑊 ∧ (𝐹 ↾ (0..^𝑁)) ≠ ∅)) | 
| 30 | 18, 28, 29 | sylanbrc 583 | . 2
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ∈ (Word 𝑊 ∖ {∅})) | 
| 31 |  | lbfzo0 13740 | . . . . 5
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) | 
| 32 | 22, 31 | sylibr 234 | . . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → 0 ∈ (0..^𝑁)) | 
| 33 | 32 | fvresd 6925 | . . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → ((𝐹 ↾ (0..^𝑁))‘0) = (𝐹‘0)) | 
| 34 | 7 | simp2bi 1146 | . . . 4
⊢ (𝐹 ∈ dom 𝑆 → (𝐹‘0) ∈ 𝐷) | 
| 35 | 34 | adantr 480 | . . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹‘0) ∈ 𝐷) | 
| 36 | 33, 35 | eqeltrd 2840 | . 2
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → ((𝐹 ↾ (0..^𝑁))‘0) ∈ 𝐷) | 
| 37 |  | elfzuz3 13562 | . . . . . . 7
⊢ (𝑁 ∈
(1...(♯‘𝐹))
→ (♯‘𝐹)
∈ (ℤ≥‘𝑁)) | 
| 38 | 37 | adantl 481 | . . . . . 6
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (♯‘𝐹) ∈
(ℤ≥‘𝑁)) | 
| 39 |  | fzoss2 13728 | . . . . . 6
⊢
((♯‘𝐹)
∈ (ℤ≥‘𝑁) → (1..^𝑁) ⊆ (1..^(♯‘𝐹))) | 
| 40 | 38, 39 | syl 17 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (1..^𝑁) ⊆
(1..^(♯‘𝐹))) | 
| 41 | 7 | simp3bi 1147 | . . . . . 6
⊢ (𝐹 ∈ dom 𝑆 → ∀𝑖 ∈ (1..^(♯‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))) | 
| 42 | 41 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → ∀𝑖 ∈
(1..^(♯‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))) | 
| 43 |  | ssralv 4051 | . . . . 5
⊢
((1..^𝑁) ⊆
(1..^(♯‘𝐹))
→ (∀𝑖 ∈
(1..^(♯‘𝐹))(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))) → ∀𝑖 ∈ (1..^𝑁)(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) | 
| 44 | 40, 42, 43 | sylc 65 | . . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → ∀𝑖 ∈ (1..^𝑁)(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))) | 
| 45 |  | fzo0ss1 13730 | . . . . . . . 8
⊢
(1..^𝑁) ⊆
(0..^𝑁) | 
| 46 | 45 | sseli 3978 | . . . . . . 7
⊢ (𝑖 ∈ (1..^𝑁) → 𝑖 ∈ (0..^𝑁)) | 
| 47 | 46 | fvresd 6925 | . . . . . 6
⊢ (𝑖 ∈ (1..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑖) = (𝐹‘𝑖)) | 
| 48 |  | elfzoel2 13699 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1..^𝑁) → 𝑁 ∈ ℤ) | 
| 49 |  | peano2zm 12662 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) | 
| 50 | 48, 49 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (1..^𝑁) → (𝑁 − 1) ∈ ℤ) | 
| 51 |  | uzid 12894 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) | 
| 52 | 48, 51 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1..^𝑁) → 𝑁 ∈ (ℤ≥‘𝑁)) | 
| 53 | 48 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1..^𝑁) → 𝑁 ∈ ℂ) | 
| 54 |  | ax-1cn 11214 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ | 
| 55 |  | npcan 11518 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) | 
| 56 | 53, 54, 55 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1..^𝑁) → ((𝑁 − 1) + 1) = 𝑁) | 
| 57 | 56 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1..^𝑁) →
(ℤ≥‘((𝑁 − 1) + 1)) =
(ℤ≥‘𝑁)) | 
| 58 | 52, 57 | eleqtrrd 2843 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (1..^𝑁) → 𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) | 
| 59 |  | peano2uzr 12946 | . . . . . . . . . . . 12
⊢ (((𝑁 − 1) ∈ ℤ ∧
𝑁 ∈
(ℤ≥‘((𝑁 − 1) + 1))) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) | 
| 60 | 50, 58, 59 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (1..^𝑁) → 𝑁 ∈ (ℤ≥‘(𝑁 − 1))) | 
| 61 |  | fzoss2 13728 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 1)) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) | 
| 62 | 60, 61 | syl 17 | . . . . . . . . . 10
⊢ (𝑖 ∈ (1..^𝑁) → (0..^(𝑁 − 1)) ⊆ (0..^𝑁)) | 
| 63 |  | elfzo1elm1fzo0 13808 | . . . . . . . . . 10
⊢ (𝑖 ∈ (1..^𝑁) → (𝑖 − 1) ∈ (0..^(𝑁 − 1))) | 
| 64 | 62, 63 | sseldd 3983 | . . . . . . . . 9
⊢ (𝑖 ∈ (1..^𝑁) → (𝑖 − 1) ∈ (0..^𝑁)) | 
| 65 | 64 | fvresd 6925 | . . . . . . . 8
⊢ (𝑖 ∈ (1..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1)) = (𝐹‘(𝑖 − 1))) | 
| 66 | 65 | fveq2d 6909 | . . . . . . 7
⊢ (𝑖 ∈ (1..^𝑁) → (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1))) = (𝑇‘(𝐹‘(𝑖 − 1)))) | 
| 67 | 66 | rneqd 5948 | . . . . . 6
⊢ (𝑖 ∈ (1..^𝑁) → ran (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1))) = ran (𝑇‘(𝐹‘(𝑖 − 1)))) | 
| 68 | 47, 67 | eleq12d 2834 | . . . . 5
⊢ (𝑖 ∈ (1..^𝑁) → (((𝐹 ↾ (0..^𝑁))‘𝑖) ∈ ran (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1))) ↔ (𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1))))) | 
| 69 | 68 | ralbiia 3090 | . . . 4
⊢
(∀𝑖 ∈
(1..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑖) ∈ ran (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1))) ↔ ∀𝑖 ∈ (1..^𝑁)(𝐹‘𝑖) ∈ ran (𝑇‘(𝐹‘(𝑖 − 1)))) | 
| 70 | 44, 69 | sylibr 234 | . . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → ∀𝑖 ∈ (1..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑖) ∈ ran (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1)))) | 
| 71 | 15 | fveq2d 6909 | . . . . 5
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (♯‘(𝐹 prefix 𝑁)) = (♯‘(𝐹 ↾ (0..^𝑁)))) | 
| 72 | 71, 20 | eqtr3d 2778 | . . . 4
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁) | 
| 73 | 72 | oveq2d 7448 | . . 3
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) →
(1..^(♯‘(𝐹
↾ (0..^𝑁)))) =
(1..^𝑁)) | 
| 74 | 70, 73 | raleqtrrdv 3329 | . 2
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → ∀𝑖 ∈
(1..^(♯‘(𝐹
↾ (0..^𝑁))))((𝐹 ↾ (0..^𝑁))‘𝑖) ∈ ran (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1)))) | 
| 75 | 1, 2, 3, 4, 5, 6 | efgsdm 19749 | . 2
⊢ ((𝐹 ↾ (0..^𝑁)) ∈ dom 𝑆 ↔ ((𝐹 ↾ (0..^𝑁)) ∈ (Word 𝑊 ∖ {∅}) ∧ ((𝐹 ↾ (0..^𝑁))‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(♯‘(𝐹 ↾ (0..^𝑁))))((𝐹 ↾ (0..^𝑁))‘𝑖) ∈ ran (𝑇‘((𝐹 ↾ (0..^𝑁))‘(𝑖 − 1))))) | 
| 76 | 30, 36, 74, 75 | syl3anbrc 1343 | 1
⊢ ((𝐹 ∈ dom 𝑆 ∧ 𝑁 ∈ (1...(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) ∈ dom 𝑆) |