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 ⊢S∈WordB∧T∈WordB∧I∈0..^T→S++T⁡I+S=T⁡I

Proof

Step Hyp Ref Expression
1 lencl ⊢S∈WordB→S∈ℕ0
2 1 nn0zd ⊢S∈WordB→S∈ℤ
3 2 anim1ci ⊢S∈WordB∧I∈0..^T→I∈0..^T∧S∈ℤ
4 3 3adant2 ⊢S∈WordB∧T∈WordB∧I∈0..^T→I∈0..^T∧S∈ℤ
5 fzo0addelr ⊢I∈0..^T∧S∈ℤ→I+S∈S..^S+T
6 4 5 syl ⊢S∈WordB∧T∈WordB∧I∈0..^T→I+S∈S..^S+T
7 ccatval2 ⊢S∈WordB∧T∈WordB∧I+S∈S..^S+T→S++T⁡I+S=T⁡I+S-S
8 6 7 syld3an3 ⊢S∈WordB∧T∈WordB∧I∈0..^T→S++T⁡I+S=T⁡I+S-S
9 elfzoelz ⊢I∈0..^T→I∈ℤ
10 9 3ad2ant3 ⊢S∈WordB∧T∈WordB∧I∈0..^T→I∈ℤ
11 10 zcnd ⊢S∈WordB∧T∈WordB∧I∈0..^T→I∈ℂ
12 1 3ad2ant1 ⊢S∈WordB∧T∈WordB∧I∈0..^T→S∈ℕ0
13 12 nn0cnd ⊢S∈WordB∧T∈WordB∧I∈0..^T→S∈ℂ
14 11 13 pncand ⊢S∈WordB∧T∈WordB∧I∈0..^T→I+S-S=I
15 14 fveq2d ⊢S∈WordB∧T∈WordB∧I∈0..^T→T⁡I+S-S=T⁡I
16 8 15 eqtrd ⊢S∈WordB∧T∈WordB∧I∈0..^T→S++T⁡I+S=T⁡I