Metamath Proof Explorer

Theorem ccatval1

Description: Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 22-Sep-2015) (Proof shortened by AV, 30-Apr-2020) (Revised by JJ, 18-Jan-2024)

Ref Expression
Assertion ccatval1 ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → S ++ T ⁡ I = S ⁡ I

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ S ∈ Word A ∧ T ∈ Word B → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
2 1 3adant3 ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
3 eleq1 ⊢ x = I → x ∈ 0 ..^ S ↔ I ∈ 0 ..^ S
4 fveq2 ⊢ x = I → S ⁡ x = S ⁡ I
5 fvoveq1 ⊢ x = I → T ⁡ x − S = T ⁡ I − S
6 3 4 5 ifbieq12d ⊢ x = I → if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S = if I ∈ 0 ..^ S S ⁡ I T ⁡ I − S
7 iftrue ⊢ I ∈ 0 ..^ S → if I ∈ 0 ..^ S S ⁡ I T ⁡ I − S = S ⁡ I
8 7 3ad2ant3 ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → if I ∈ 0 ..^ S S ⁡ I T ⁡ I − S = S ⁡ I
9 6 8 sylan9eqr ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S ∧ x = I → if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S = S ⁡ I
10 id ⊢ I ∈ 0 ..^ S → I ∈ 0 ..^ S
11 lencl ⊢ T ∈ Word B → T ∈ ℕ 0
12 elfzoext ⊢ I ∈ 0 ..^ S ∧ T ∈ ℕ 0 → I ∈ 0 ..^ S + T
13 10 11 12 syl2anr ⊢ T ∈ Word B ∧ I ∈ 0 ..^ S → I ∈ 0 ..^ S + T
14 13 3adant1 ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → I ∈ 0 ..^ S + T
15 fvexd ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → S ⁡ I ∈ V
16 2 9 14 15 fvmptd ⊢ S ∈ Word A ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → S ++ T ⁡ I = S ⁡ I