Step |
Hyp |
Ref |
Expression |
1 |
|
ccatfval |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) |
3 |
|
eleq1 |
⊢ ( 𝑥 = 𝐼 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ↔ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝑥 = 𝐼 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐼 ) ) |
5 |
|
fvoveq1 |
⊢ ( 𝑥 = 𝐼 → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) |
6 |
3 4 5
|
ifbieq12d |
⊢ ( 𝑥 = 𝐼 → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) = if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) ) |
7 |
|
iftrue |
⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑆 ‘ 𝐼 ) ) |
8 |
7
|
3ad2ant3 |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → if ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝐼 ) , ( 𝑇 ‘ ( 𝐼 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑆 ‘ 𝐼 ) ) |
9 |
6 8
|
sylan9eqr |
⊢ ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ∧ 𝑥 = 𝐼 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝑆 ‘ 𝐼 ) ) |
10 |
|
id |
⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) |
11 |
|
lencl |
⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) |
12 |
|
elfzoext |
⊢ ( ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) |
13 |
10 11 12
|
syl2anr |
⊢ ( ( 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) |
14 |
13
|
3adant1 |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) |
15 |
|
fvexd |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝐼 ) ∈ V ) |
16 |
2 9 14 15
|
fvmptd |
⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝐼 ) = ( 𝑆 ‘ 𝐼 ) ) |