Proof of Theorem swrdccat3b
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
2 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) |
3 | | elfzubelfz 12353 |
. . . . 5
⊢ (𝑀 ∈ (0...(𝐿 + (#‘𝐵))) → (𝐿 + (#‘𝐵)) ∈ (0...(𝐿 + (#‘𝐵)))) |
4 | 3 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → (𝐿 + (#‘𝐵)) ∈ (0...(𝐿 + (#‘𝐵)))) |
5 | | swrdccatin12.l |
. . . . . 6
⊢ 𝐿 = (#‘𝐴) |
6 | 5 | swrdccat3 13492 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...(𝐿 + (#‘𝐵))) ∧ (𝐿 + (#‘𝐵)) ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (#‘𝐵))〉) = if((𝐿 + (#‘𝐵)) ≤ 𝐿, (𝐴 substr 〈𝑀, (𝐿 + (#‘𝐵))〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉)))))) |
7 | 6 | imp 445 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...(𝐿 + (#‘𝐵))) ∧ (𝐿 + (#‘𝐵)) ∈ (0...(𝐿 + (#‘𝐵))))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (#‘𝐵))〉) = if((𝐿 + (#‘𝐵)) ≤ 𝐿, (𝐴 substr 〈𝑀, (𝐿 + (#‘𝐵))〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉))))) |
8 | 1, 2, 4, 7 | syl12anc 1324 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (#‘𝐵))〉) = if((𝐿 + (#‘𝐵)) ≤ 𝐿, (𝐴 substr 〈𝑀, (𝐿 + (#‘𝐵))〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉))))) |
9 | 5 | swrdccat3blem 13495 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ (𝐿 + (#‘𝐵)) ≤ 𝐿) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = (𝐴 substr 〈𝑀, (𝐿 + (#‘𝐵))〉)) |
10 | | iftrue 4092 |
. . . . . 6
⊢ (𝐿 ≤ 𝑀 → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉)) |
11 | 10 | 3ad2ant3 1084 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉)) |
12 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
13 | 12 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈ ℂ) |
14 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈
ℕ0) |
15 | 14 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Word 𝑉 → (#‘𝐵) ∈ ℂ) |
16 | 5 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢
(#‘𝐴) = 𝐿 |
17 | 16 | eleq1i 2692 |
. . . . . . . . . . . 12
⊢
((#‘𝐴) ∈
ℂ ↔ 𝐿 ∈
ℂ) |
18 | | pncan2 10288 |
. . . . . . . . . . . 12
⊢ ((𝐿 ∈ ℂ ∧
(#‘𝐵) ∈ ℂ)
→ ((𝐿 + (#‘𝐵)) − 𝐿) = (#‘𝐵)) |
19 | 17, 18 | sylanb 489 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((𝐿
+ (#‘𝐵)) −
𝐿) = (#‘𝐵)) |
20 | 13, 15, 19 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + (#‘𝐵)) − 𝐿) = (#‘𝐵)) |
21 | 20 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (#‘𝐵) = ((𝐿 + (#‘𝐵)) − 𝐿)) |
22 | 21 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → (#‘𝐵) = ((𝐿 + (#‘𝐵)) − 𝐿)) |
23 | 22 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (#‘𝐵) = ((𝐿 + (#‘𝐵)) − 𝐿)) |
24 | 23 | opeq2d 4409 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → 〈(𝑀 − 𝐿), (#‘𝐵)〉 = 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉) |
25 | 24 | oveq2d 6666 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉) = (𝐵 substr 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉)) |
26 | 11, 25 | eqtrd 2656 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ 𝐿 ≤ 𝑀) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = (𝐵 substr 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉)) |
27 | | iffalse 4095 |
. . . . . 6
⊢ (¬
𝐿 ≤ 𝑀 → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) |
28 | 27 | 3ad2ant3 1084 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) |
29 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐿 + (#‘𝐵)) − 𝐿) = (#‘𝐵)) |
30 | 29 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐿 + (#‘𝐵)) − 𝐿) = (#‘𝐵)) |
31 | 30 | opeq2d 4409 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉 = 〈0, (#‘𝐵)〉) |
32 | 31 | oveq2d 6666 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉) = (𝐵 substr 〈0, (#‘𝐵)〉)) |
33 | | swrdid 13428 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Word 𝑉 → (𝐵 substr 〈0, (#‘𝐵)〉) = 𝐵) |
34 | 33 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐵 substr 〈0, (#‘𝐵)〉) = 𝐵) |
35 | 34 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → (𝐵 substr 〈0, (#‘𝐵)〉) = 𝐵) |
36 | 35 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → (𝐵 substr 〈0, (#‘𝐵)〉) = 𝐵) |
37 | 32, 36 | eqtr2d 2657 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → 𝐵 = (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉)) |
38 | 37 | oveq2d 6666 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉))) |
39 | 28, 38 | eqtrd 2656 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) ∧ ¬ (𝐿 + (#‘𝐵)) ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉))) |
40 | 9, 26, 39 | 2if2 4136 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)) = if((𝐿 + (#‘𝐵)) ≤ 𝐿, (𝐴 substr 〈𝑀, (𝐿 + (#‘𝐵))〉), if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), ((𝐿 + (#‘𝐵)) − 𝐿)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ (𝐵 substr 〈0, ((𝐿 + (#‘𝐵)) − 𝐿)〉))))) |
41 | 8, 40 | eqtr4d 2659 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝑀 ∈ (0...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (#‘𝐵))〉) = if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵))) |
42 | 41 | ex 450 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑀 ∈ (0...(𝐿 + (#‘𝐵))) → ((𝐴 ++ 𝐵) substr 〈𝑀, (𝐿 + (#‘𝐵))〉) = if(𝐿 ≤ 𝑀, (𝐵 substr 〈(𝑀 − 𝐿), (#‘𝐵)〉), ((𝐴 substr 〈𝑀, 𝐿〉) ++ 𝐵)))) |