Step | Hyp | Ref
| Expression |
1 | | lencl 14428 |
. . . . . . . 8
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈
ℕ0) |
2 | | nn0le0eq0 12448 |
. . . . . . . . 9
⊢
((♯‘𝐵)
∈ ℕ0 → ((♯‘𝐵) ≤ 0 ↔ (♯‘𝐵) = 0)) |
3 | 2 | biimpd 228 |
. . . . . . . 8
⊢
((♯‘𝐵)
∈ ℕ0 → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0)) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0)) |
5 | 4 | adantl 483 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) ≤ 0 → (♯‘𝐵) = 0)) |
6 | | hasheq0 14270 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) = 0 ↔ 𝐵 = ∅)) |
7 | 6 | biimpd 228 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Word 𝑉 → ((♯‘𝐵) = 0 → 𝐵 = ∅)) |
8 | 7 | adantl 483 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) = 0 → 𝐵 = ∅)) |
9 | 8 | imp 408 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) → 𝐵 = ∅) |
10 | | lencl 14428 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
11 | | swrdccatin2.l |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐿 = (♯‘𝐴) |
12 | 11 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘𝐴) =
𝐿 |
13 | 12 | eleq1i 2829 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘𝐴)
∈ ℕ0 ↔ 𝐿 ∈
ℕ0) |
14 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
15 | | elfz2nn0 13539 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ (0...(𝐿 + 0)) ↔ (𝑀 ∈ ℕ0 ∧ (𝐿 + 0) ∈ ℕ0
∧ 𝑀 ≤ (𝐿 + 0))) |
16 | | recn 11148 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐿 ∈ ℝ → 𝐿 ∈
ℂ) |
17 | 16 | addid1d 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐿 ∈ ℝ → (𝐿 + 0) = 𝐿) |
18 | 17 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐿 ∈ ℝ → (𝑀 ≤ (𝐿 + 0) ↔ 𝑀 ≤ 𝐿)) |
19 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
20 | 19 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈ ℝ)
→ (𝑀 ∈ ℝ
∧ 𝐿 ∈
ℝ)) |
21 | 20 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 ∈ ℝ
∧ 𝐿 ∈
ℝ)) |
22 | | letri3 11247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 = 𝐿 ↔ (𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 = 𝐿 ↔ (𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀))) |
24 | 23 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ ((𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 𝑀 = 𝐿)) |
25 | 24 | exp4b 432 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐿 ∈ ℝ → (𝑀 ∈ ℕ0
→ (𝑀 ≤ 𝐿 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))) |
26 | 25 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐿 ∈ ℝ → (𝑀 ≤ 𝐿 → (𝑀 ∈ ℕ0 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))) |
27 | 18, 26 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐿 ∈ ℝ → (𝑀 ≤ (𝐿 + 0) → (𝑀 ∈ ℕ0 → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))) |
28 | 27 | com3l 89 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ≤ (𝐿 + 0) → (𝑀 ∈ ℕ0 → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)))) |
29 | 28 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ0
∧ 𝑀 ≤ (𝐿 + 0)) → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
30 | 29 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ0
∧ (𝐿 + 0) ∈
ℕ0 ∧ 𝑀
≤ (𝐿 + 0)) → (𝐿 ∈ ℝ → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
31 | 30 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℝ → ((𝑀 ∈ ℕ0
∧ (𝐿 + 0) ∈
ℕ0 ∧ 𝑀
≤ (𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
32 | 15, 31 | biimtrid 241 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ ℝ → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
33 | 14, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ ℕ0
→ (𝑀 ∈
(0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
34 | 13, 33 | sylbi 216 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘𝐴)
∈ ℕ0 → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
35 | 10, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑉 → (𝑀 ∈ (0...(𝐿 + 0)) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿))) |
36 | 35 | imp 408 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐿 ≤ 𝑀 → 𝑀 = 𝐿)) |
37 | | elfznn0 13541 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ (0...(𝐿 + 0)) → 𝑀 ∈
ℕ0) |
38 | | swrd00 14539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∅
substr ⟨0, 0⟩) = ∅ |
39 | | swrd00 14539 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 substr ⟨𝐿, 𝐿⟩) = ∅ |
40 | 38, 39 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∅
substr ⟨0, 0⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩) |
41 | | nn0cn 12430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℂ) |
42 | 41 | subidd 11507 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐿 ∈ ℕ0
→ (𝐿 − 𝐿) = 0) |
43 | 42 | opeq1d 4841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐿 ∈ ℕ0
→ ⟨(𝐿 −
𝐿), 0⟩ = ⟨0,
0⟩) |
44 | 43 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ ℕ0
→ (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (∅ substr ⟨0,
0⟩)) |
45 | 41 | addid1d 11362 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 0) = 𝐿) |
46 | 45 | opeq2d 4842 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐿 ∈ ℕ0
→ ⟨𝐿, (𝐿 + 0)⟩ = ⟨𝐿, 𝐿⟩) |
47 | 46 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐿 ∈ ℕ0
→ (𝐴 substr
⟨𝐿, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, 𝐿⟩)) |
48 | 40, 44, 47 | 3eqtr4a 2803 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ ℕ0
→ (∅ substr ⟨(𝐿 − 𝐿), 0⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩)) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 = 𝐿 → (𝐿 ∈ ℕ0 → (∅
substr ⟨(𝐿 −
𝐿), 0⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩))) |
50 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 = 𝐿 → (𝑀 ∈ ℕ0 ↔ 𝐿 ∈
ℕ0)) |
51 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 = 𝐿 → (𝑀 − 𝐿) = (𝐿 − 𝐿)) |
52 | 51 | opeq1d 4841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 = 𝐿 → ⟨(𝑀 − 𝐿), 0⟩ = ⟨(𝐿 − 𝐿), 0⟩) |
53 | 52 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (∅ substr ⟨(𝐿 − 𝐿), 0⟩)) |
54 | | opeq1 4835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 = 𝐿 → ⟨𝑀, (𝐿 + 0)⟩ = ⟨𝐿, (𝐿 + 0)⟩) |
55 | 54 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 = 𝐿 → (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩)) |
56 | 53, 55 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 = 𝐿 → ((∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩) ↔ (∅ substr
⟨(𝐿 − 𝐿), 0⟩) = (𝐴 substr ⟨𝐿, (𝐿 + 0)⟩))) |
57 | 49, 50, 56 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 = 𝐿 → (𝑀 ∈ ℕ0 → (∅
substr ⟨(𝑀 −
𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
58 | 57 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ (𝑀 = 𝐿 → (∅ substr
⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
59 | 58 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ0
→ (𝐴 ∈ Word 𝑉 → (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))) |
60 | 37, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ (0...(𝐿 + 0)) → (𝐴 ∈ Word 𝑉 → (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))) |
61 | 60 | impcom 409 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝑀 = 𝐿 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
62 | 36, 61 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → (𝐿 ≤ 𝑀 → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
63 | 62 | imp 408 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) ∧ 𝐿 ≤ 𝑀) → (∅ substr ⟨(𝑀 − 𝐿), 0⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
64 | | swrdcl 14540 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉) |
65 | | ccatrid 14482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 substr ⟨𝑀, 𝐿⟩) ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝐿⟩)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝐿⟩)) |
67 | 13, 41 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝐴)
∈ ℕ0 → 𝐿 ∈ ℂ) |
68 | 10, 67 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℂ) |
69 | | addid1 11342 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℂ → (𝐿 + 0) = 𝐿) |
70 | 69 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ ℂ → 𝐿 = (𝐿 + 0)) |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 = (𝐿 + 0)) |
72 | 71 | opeq2d 4842 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Word 𝑉 → ⟨𝑀, 𝐿⟩ = ⟨𝑀, (𝐿 + 0)⟩) |
73 | 72 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨𝑀, 𝐿⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
74 | 66, 73 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
76 | 75 | adantr 482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
77 | 63, 76 | ifeqda 4527 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(𝐿 + 0))) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
78 | 77 | ex 414 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
79 | 78 | ad3antrrr 729 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
80 | | oveq2 7370 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐵) =
0 → (𝐿 +
(♯‘𝐵)) = (𝐿 + 0)) |
81 | 80 | oveq2d 7378 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐵) =
0 → (0...(𝐿 +
(♯‘𝐵))) =
(0...(𝐿 +
0))) |
82 | 81 | eleq2d 2824 |
. . . . . . . . . . . 12
⊢
((♯‘𝐵) =
0 → (𝑀 ∈
(0...(𝐿 +
(♯‘𝐵))) ↔
𝑀 ∈ (0...(𝐿 + 0)))) |
83 | 82 | adantr 482 |
. . . . . . . . . . 11
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ (𝑀 ∈
(0...(𝐿 +
(♯‘𝐵))) ↔
𝑀 ∈ (0...(𝐿 + 0)))) |
84 | | simpr 486 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ 𝐵 =
∅) |
85 | | opeq2 4836 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐵) =
0 → ⟨(𝑀 −
𝐿), (♯‘𝐵)⟩ = ⟨(𝑀 − 𝐿), 0⟩) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ ⟨(𝑀 −
𝐿), (♯‘𝐵)⟩ = ⟨(𝑀 − 𝐿), 0⟩) |
87 | 84, 86 | oveq12d 7380 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ (𝐵 substr
⟨(𝑀 − 𝐿), (♯‘𝐵)⟩) = (∅ substr
⟨(𝑀 − 𝐿), 0⟩)) |
88 | | oveq2 7370 |
. . . . . . . . . . . . . 14
⊢ (𝐵 = ∅ → ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ ((𝐴 substr
⟨𝑀, 𝐿⟩) ++ 𝐵) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) |
90 | 87, 89 | ifeq12d 4512 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅))) |
91 | 80 | opeq2d 4842 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐵) =
0 → ⟨𝑀, (𝐿 + (♯‘𝐵))⟩ = ⟨𝑀, (𝐿 + 0)⟩) |
92 | 91 | oveq2d 7378 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐵) =
0 → (𝐴 substr
⟨𝑀, (𝐿 + (♯‘𝐵))⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
93 | 92 | adantr 482 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ (𝐴 substr
⟨𝑀, (𝐿 + (♯‘𝐵))⟩) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)) |
94 | 90, 93 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ (if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩) ↔ if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩))) |
95 | 83, 94 | imbi12d 345 |
. . . . . . . . . 10
⊢
(((♯‘𝐵)
= 0 ∧ 𝐵 = ∅)
→ ((𝑀 ∈
(0...(𝐿 +
(♯‘𝐵))) →
if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)) ↔ (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))) |
96 | 95 | adantll 713 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → ((𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)) ↔ (𝑀 ∈ (0...(𝐿 + 0)) → if(𝐿 ≤ 𝑀, (∅ substr ⟨(𝑀 − 𝐿), 0⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ ∅)) = (𝐴 substr ⟨𝑀, (𝐿 + 0)⟩)))) |
97 | 79, 96 | mpbird 257 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) ∧ 𝐵 = ∅) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))) |
98 | 9, 97 | mpdan 686 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (♯‘𝐵) = 0) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))) |
99 | 98 | ex 414 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) = 0 → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))) |
100 | 5, 99 | syld 47 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐵) ≤ 0 → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))) |
101 | 100 | com23 86 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑀 ∈ (0...(𝐿 + (♯‘𝐵))) → ((♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))) |
102 | 101 | imp 408 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))) |
103 | 102 | adantr 482 |
. 2
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → ((♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))) |
104 | 11 | eleq1i 2829 |
. . . . . . . 8
⊢ (𝐿 ∈ ℕ0
↔ (♯‘𝐴)
∈ ℕ0) |
105 | 104, 14 | sylbir 234 |
. . . . . . 7
⊢
((♯‘𝐴)
∈ ℕ0 → 𝐿 ∈ ℝ) |
106 | 10, 105 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℝ) |
107 | 1 | nn0red 12481 |
. . . . . 6
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℝ) |
108 | | leaddle0 11677 |
. . . . . 6
⊢ ((𝐿 ∈ ℝ ∧
(♯‘𝐵) ∈
ℝ) → ((𝐿 +
(♯‘𝐵)) ≤
𝐿 ↔
(♯‘𝐵) ≤
0)) |
109 | 106, 107,
108 | syl2an 597 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 ↔ (♯‘𝐵) ≤ 0)) |
110 | | pm2.24 124 |
. . . . 5
⊢
((♯‘𝐵)
≤ 0 → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))) |
111 | 109, 110 | syl6bi 253 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))) |
112 | 111 | adantr 482 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐿 + (♯‘𝐵)) ≤ 𝐿 → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)))) |
113 | 112 | imp 408 |
. 2
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → (¬ (♯‘𝐵) ≤ 0 → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩))) |
114 | 103, 113 | pm2.61d 179 |
1
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (♯‘𝐵)))) ∧ (𝐿 + (♯‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr ⟨(𝑀 − 𝐿), (♯‘𝐵)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ 𝐵)) = (𝐴 substr ⟨𝑀, (𝐿 + (♯‘𝐵))⟩)) |