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

Proof

Step Hyp Ref Expression
1 ccatfval ⊢S∈WordA∧T∈WordB→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S
2 1 3adant3 ⊢S∈WordA∧T∈WordB∧I∈0..^S→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡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→ifx∈0..^SS⁡xT⁡x−S=ifI∈0..^SS⁡IT⁡I−S
7 iftrue ⊢I∈0..^S→ifI∈0..^SS⁡IT⁡I−S=S⁡I
8 7 3ad2ant3 ⊢S∈WordA∧T∈WordB∧I∈0..^S→ifI∈0..^SS⁡IT⁡I−S=S⁡I
9 6 8 sylan9eqr ⊢S∈WordA∧T∈WordB∧I∈0..^S∧x=I→ifx∈0..^SS⁡xT⁡x−S=S⁡I
10 id ⊢I∈0..^S→I∈0..^S
11 lencl ⊢T∈WordB→T∈ℕ0
12 elfzoext ⊢I∈0..^S∧T∈ℕ0→I∈0..^S+T
13 10 11 12 syl2anr ⊢T∈WordB∧I∈0..^S→I∈0..^S+T
14 13 3adant1 ⊢S∈WordA∧T∈WordB∧I∈0..^S→I∈0..^S+T
15 fvexd ⊢S∈WordA∧T∈WordB∧I∈0..^S→S⁡I∈V
16 2 9 14 15 fvmptd ⊢S∈WordA∧T∈WordB∧I∈0..^S→S++T⁡I=S⁡I