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

Proof

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