Proof of Theorem swrdccat3a
Step | Hyp | Ref
| Expression |
1 | | elfznn0 12433 |
. . . . . 6
⊢ (𝑁 ∈ (0...(𝐿 + (#‘𝐵))) → 𝑁 ∈
ℕ0) |
2 | | 0elfz 12436 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ (0...(𝐿 + (#‘𝐵))) → 0 ∈ (0...𝑁)) |
4 | 3 | ancri 575 |
. . . 4
⊢ (𝑁 ∈ (0...(𝐿 + (#‘𝐵))) → (0 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵))))) |
5 | | swrdccatin12.l |
. . . . . 6
⊢ 𝐿 = (#‘𝐴) |
6 | 5 | swrdccat3 13492 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((0 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), if(𝐿 ≤ 0, (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)))))) |
7 | 6 | imp 445 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (0 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), if(𝐿 ≤ 0, (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))))) |
8 | 4, 7 | sylan2 491 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), if(𝐿 ≤ 0, (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))))) |
9 | | iftrue 4092 |
. . . . 5
⊢ (𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = (𝐴 substr 〈0, 𝑁〉)) |
10 | 9 | adantl 482 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ 𝑁 ≤ 𝐿) → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = (𝐴 substr 〈0, 𝑁〉)) |
11 | | iffalse 4095 |
. . . . . 6
⊢ (¬
𝑁 ≤ 𝐿 → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) |
12 | 11 | 3ad2ant2 1083 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 0) → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) |
13 | | lencl 13324 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
14 | 5, 13 | syl5eqel 2705 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) |
15 | | nn0le0eq0 11321 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ ℕ0
→ (𝐿 ≤ 0 ↔
𝐿 = 0)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (𝐿 ≤ 0 ↔ 𝐿 = 0)) |
17 | 16 | biimpd 219 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (𝐿 ≤ 0 → 𝐿 = 0)) |
18 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ≤ 0 → 𝐿 = 0)) |
19 | 5 | eqeq1i 2627 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 = 0 ↔ (#‘𝐴) = 0) |
20 | 19 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 = 0 → (#‘𝐴) = 0) |
21 | | hasheq0 13154 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑉 → ((#‘𝐴) = 0 ↔ 𝐴 = ∅)) |
22 | 20, 21 | syl5ib 234 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Word 𝑉 → (𝐿 = 0 → 𝐴 = ∅)) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 = 0 → 𝐴 = ∅)) |
24 | 23 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → 𝐴 = ∅) |
25 | | 0m0e0 11130 |
. . . . . . . . . . . . . . . 16
⊢ (0
− 0) = 0 |
26 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (0 =
𝐿 → (0 − 0) = (0
− 𝐿)) |
27 | 26 | eqcoms 2630 |
. . . . . . . . . . . . . . . 16
⊢ (𝐿 = 0 → (0 − 0) = (0
− 𝐿)) |
28 | 25, 27 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 = 0 → 0 = (0 − 𝐿)) |
29 | 28 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → 0 = (0 − 𝐿)) |
30 | 29 | opeq1d 4408 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → 〈0, (𝑁 − 𝐿)〉 = 〈(0 − 𝐿), (𝑁 − 𝐿)〉) |
31 | 30 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → (𝐵 substr 〈0, (𝑁 − 𝐿)〉) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
32 | 24, 31 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (∅ ++ (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉))) |
33 | | swrdcl 13419 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ Word 𝑉 → (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉) ∈ Word 𝑉) |
34 | | ccatlid 13369 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉) ∈ Word 𝑉 → (∅ ++ (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ Word 𝑉 → (∅ ++ (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
36 | 35 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (∅ ++ (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
37 | 36 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → (∅ ++ (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
38 | 32, 37 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐿 = 0) → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
39 | 38 | ex 450 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 = 0 → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉))) |
40 | 18, 39 | syld 47 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐿 ≤ 0 → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉))) |
41 | 40 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → (𝐿 ≤ 0 → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉))) |
42 | 41 | imp 445 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ 𝐿 ≤ 0) → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
43 | 42 | 3adant2 1080 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 0) → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
44 | 12, 43 | eqtrd 2656 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 0) → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉)) |
45 | 11 | 3ad2ant2 1083 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 0) → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) |
46 | 5 | opeq2i 4406 |
. . . . . . . . . . 11
⊢ 〈0,
𝐿〉 = 〈0,
(#‘𝐴)〉 |
47 | 46 | oveq2i 6661 |
. . . . . . . . . 10
⊢ (𝐴 substr 〈0, 𝐿〉) = (𝐴 substr 〈0, (#‘𝐴)〉) |
48 | | swrdid 13428 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, (#‘𝐴)〉) = 𝐴) |
49 | 47, 48 | syl5req 2669 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑉 → 𝐴 = (𝐴 substr 〈0, 𝐿〉)) |
50 | 49 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 = (𝐴 substr 〈0, 𝐿〉)) |
51 | 50 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → 𝐴 = (𝐴 substr 〈0, 𝐿〉)) |
52 | 51 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 0) → 𝐴 = (𝐴 substr 〈0, 𝐿〉)) |
53 | 52 | oveq1d 6665 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 0) → (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) |
54 | 45, 53 | eqtrd 2656 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 0) → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) |
55 | 10, 44, 54 | 2if2 4136 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), if(𝐿 ≤ 0, (𝐵 substr 〈(0 − 𝐿), (𝑁 − 𝐿)〉), ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))))) |
56 | 8, 55 | eqtr4d 2659 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑁 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉)))) |
57 | 56 | ex 450 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(𝐿 + (#‘𝐵))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = if(𝑁 ≤ 𝐿, (𝐴 substr 〈0, 𝑁〉), (𝐴 ++ (𝐵 substr 〈0, (𝑁 − 𝐿)〉))))) |