Metamath Proof Explorer

Theorem ccatval2

Description: Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Assertion ccatval2 ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→S++T⁡I=T⁡I−S

Proof

Step Hyp Ref Expression
1 ccatfval ⊢S∈WordB∧T∈WordB→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S
2 1 3adant3 ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→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 fzodisj ⊢0..^S∩S..^S+T=∅
8 minel ⊢I∈S..^S+T∧0..^S∩S..^S+T=∅→¬I∈0..^S
9 7 8 mpan2 ⊢I∈S..^S+T→¬I∈0..^S
10 9 3ad2ant3 ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→¬I∈0..^S
11 10 iffalsed ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→ifI∈0..^SS⁡IT⁡I−S=T⁡I−S
12 6 11 sylan9eqr ⊢S∈WordB∧T∈WordB∧I∈S..^S+T∧x=I→ifx∈0..^SS⁡xT⁡x−S=T⁡I−S
13 wrdfin ⊢S∈WordB→S∈Fin
14 13 adantr ⊢S∈WordB∧T∈WordB→S∈Fin
15 hashcl ⊢S∈Fin→S∈ℕ0
16 fzoss1 ⊢S∈ℤ≥0→S..^S+T⊆0..^S+T
17 nn0uz ⊢ℕ0=ℤ≥0
18 16 17 eleq2s ⊢S∈ℕ0→S..^S+T⊆0..^S+T
19 14 15 18 3syl ⊢S∈WordB∧T∈WordB→S..^S+T⊆0..^S+T
20 19 sseld ⊢S∈WordB∧T∈WordB→I∈S..^S+T→I∈0..^S+T
21 20 3impia ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→I∈0..^S+T
22 fvexd ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→T⁡I−S∈V
23 2 12 21 22 fvmptd ⊢S∈WordB∧T∈WordB∧I∈S..^S+T→S++T⁡I=T⁡I−S