Metamath Proof Explorer

Theorem ccatval1OLD

Description: Obsolete version of ccatval1 as of 18-Jan-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
2 1 3adant3 ⊢ S ∈ Word B ∧ 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 B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → if I ∈ 0 ..^ S S ⁡ I T ⁡ I − S = S ⁡ I
9 6 8 sylan9eqr ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S ∧ x = I → if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S = S ⁡ I
10 simp3 ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → I ∈ 0 ..^ S
11 lencl ⊢ T ∈ Word B → T ∈ ℕ 0
12 11 3ad2ant2 ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → T ∈ ℕ 0
13 elfzoext ⊢ I ∈ 0 ..^ S ∧ T ∈ ℕ 0 → I ∈ 0 ..^ S + T
14 10 12 13 syl2anc ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → I ∈ 0 ..^ S + T
15 fvexd ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → S ⁡ I ∈ V
16 2 9 14 15 fvmptd ⊢ S ∈ Word B ∧ T ∈ Word B ∧ I ∈ 0 ..^ S → S ++ T ⁡ I = S ⁡ I