Proof of Theorem lpadright
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lpadlen.1 | . . . 4
⊢ (𝜑 → 𝐿 ∈
ℕ0) | 
| 2 |  | lpadlen.2 | . . . 4
⊢ (𝜑 → 𝑊 ∈ Word 𝑆) | 
| 3 |  | lpadlen.3 | . . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑆) | 
| 4 | 1, 2, 3 | lpadval 34691 | . . 3
⊢ (𝜑 → ((𝐶 leftpad 𝑊)‘𝐿) = (((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)) | 
| 5 | 4 | fveq1d 6908 | . 2
⊢ (𝜑 → (((𝐶 leftpad 𝑊)‘𝐿)‘(𝑁 + 𝑀)) = ((((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)‘(𝑁 + 𝑀))) | 
| 6 |  | eqeq2 2749 | . . . . . 6
⊢ (0 =
if(𝐿 ≤
(♯‘𝑊), 0,
(𝐿 −
(♯‘𝑊))) →
((♯‘((0..^(𝐿
− (♯‘𝑊)))
× {𝐶})) = 0 ↔
(♯‘((0..^(𝐿
− (♯‘𝑊)))
× {𝐶})) = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊))))) | 
| 7 |  | eqeq2 2749 | . . . . . 6
⊢ ((𝐿 − (♯‘𝑊)) = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊))) → ((♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = (𝐿 − (♯‘𝑊)) ↔ (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊))))) | 
| 8 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → 𝐿 ∈
ℕ0) | 
| 9 | 2 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → 𝑊 ∈ Word 𝑆) | 
| 10 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → 𝐶 ∈ 𝑆) | 
| 11 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → 𝐿 ≤ (♯‘𝑊)) | 
| 12 | 8, 9, 10, 11 | lpadlem3 34693 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) = ∅) | 
| 13 | 12 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) =
(♯‘∅)) | 
| 14 |  | hash0 14406 | . . . . . . 7
⊢
(♯‘∅) = 0 | 
| 15 | 13, 14 | eqtrdi 2793 | . . . . . 6
⊢ ((𝜑 ∧ 𝐿 ≤ (♯‘𝑊)) → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = 0) | 
| 16 | 1 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → 𝐿 ∈
ℕ0) | 
| 17 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → 𝑊 ∈ Word 𝑆) | 
| 18 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → 𝐶 ∈ 𝑆) | 
| 19 |  | lencl 14571 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈
ℕ0) | 
| 20 | 2, 19 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) | 
| 21 | 20 | nn0red 12588 | . . . . . . . . 9
⊢ (𝜑 → (♯‘𝑊) ∈
ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → (♯‘𝑊) ∈ ℝ) | 
| 23 | 1 | nn0red 12588 | . . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → 𝐿 ∈ ℝ) | 
| 25 | 21, 23 | ltnled 11408 | . . . . . . . . 9
⊢ (𝜑 → ((♯‘𝑊) < 𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑊))) | 
| 26 | 25 | biimpar 477 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → (♯‘𝑊) < 𝐿) | 
| 27 | 22, 24, 26 | ltled 11409 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → (♯‘𝑊) ≤ 𝐿) | 
| 28 | 16, 17, 18, 27 | lpadlem2 34695 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 ≤ (♯‘𝑊)) → (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})) = (𝐿 − (♯‘𝑊))) | 
| 29 | 6, 7, 15, 28 | ifbothda 4564 | . . . . 5
⊢ (𝜑 →
(♯‘((0..^(𝐿
− (♯‘𝑊)))
× {𝐶})) = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊)))) | 
| 30 |  | lpadright.1 | . . . . 5
⊢ (𝜑 → 𝑀 = if(𝐿 ≤ (♯‘𝑊), 0, (𝐿 − (♯‘𝑊)))) | 
| 31 | 29, 30 | eqtr4d 2780 | . . . 4
⊢ (𝜑 →
(♯‘((0..^(𝐿
− (♯‘𝑊)))
× {𝐶})) = 𝑀) | 
| 32 | 31 | oveq2d 7447 | . . 3
⊢ (𝜑 → (𝑁 + (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶}))) = (𝑁 + 𝑀)) | 
| 33 | 32 | fveq2d 6910 | . 2
⊢ (𝜑 → ((((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)‘(𝑁 + (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})))) = ((((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)‘(𝑁 + 𝑀))) | 
| 34 | 3 | lpadlem1 34692 | . . 3
⊢ (𝜑 → ((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ∈ Word 𝑆) | 
| 35 |  | lpadright.2 | . . 3
⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊))) | 
| 36 |  | ccatval3 14617 | . . 3
⊢
((((0..^(𝐿 −
(♯‘𝑊))) ×
{𝐶}) ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)‘(𝑁 + (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})))) = (𝑊‘𝑁)) | 
| 37 | 34, 2, 35, 36 | syl3anc 1373 | . 2
⊢ (𝜑 → ((((0..^(𝐿 − (♯‘𝑊))) × {𝐶}) ++ 𝑊)‘(𝑁 + (♯‘((0..^(𝐿 − (♯‘𝑊))) × {𝐶})))) = (𝑊‘𝑁)) | 
| 38 | 5, 33, 37 | 3eqtr2d 2783 | 1
⊢ (𝜑 → (((𝐶 leftpad 𝑊)‘𝐿)‘(𝑁 + 𝑀)) = (𝑊‘𝑁)) |