Metamath Proof Explorer

Theorem ccatval3

Description: Value of a symbol in the right half of a concatenated word, using an index relative to the subword. (Contributed by Stefan O'Rear, 16-Aug-2015) (Proof shortened by AV, 30-Apr-2020)

Ref Expression
Assertion ccatval3 ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 lencl ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
2 1 nn0zd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℤ )
3 2 anim1ci ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℤ ) )
4 3 3adant2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℤ ) )
5 fzo0addelr ⊢ ( ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℤ ) → ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
6 4 5 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
7 ccatval2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( ( 𝐼 + ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑆 ) ) ) )
8 6 7 syld3an3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ ( ( 𝐼 + ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑆 ) ) ) )
9 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) → 𝐼 ∈ ℤ )
10 9 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝐼 ∈ ℤ )
11 10 zcnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝐼 ∈ ℂ )
12 1 3ad2ant1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
13 12 nn0cnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ℂ )
14 11 13 pncand ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝐼 + ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑆 ) ) = 𝐼 )
15 14 fveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ‘ ( ( 𝐼 + ( ♯ ‘ 𝑆 ) ) − ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ 𝐼 ) )
16 8 15 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝐼 + ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ 𝐼 ) )