Metamath Proof Explorer

Theorem ccatfval

Description: Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion ccatfval ⊢S∈V∧T∈W→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S

Proof

Step Hyp Ref Expression
1 elex ⊢S∈V→S∈V
2 elex ⊢T∈W→T∈V
3 fveq2 ⊢s=S→s=S
4 fveq2 ⊢t=T→t=T
5 3 4 oveqan12d ⊢s=S∧t=T→s+t=S+T
6 5 oveq2d ⊢s=S∧t=T→0..^s+t=0..^S+T
7 3 oveq2d ⊢s=S→0..^s=0..^S
8 7 eleq2d ⊢s=S→x∈0..^s↔x∈0..^S
9 8 adantr ⊢s=S∧t=T→x∈0..^s↔x∈0..^S
10 fveq1 ⊢s=S→s⁡x=S⁡x
11 10 adantr ⊢s=S∧t=T→s⁡x=S⁡x
12 simpr ⊢s=S∧t=T→t=T
13 3 oveq2d ⊢s=S→x−s=x−S
14 13 adantr ⊢s=S∧t=T→x−s=x−S
15 12 14 fveq12d ⊢s=S∧t=T→t⁡x−s=T⁡x−S
16 9 11 15 ifbieq12d ⊢s=S∧t=T→ifx∈0..^ss⁡xt⁡x−s=ifx∈0..^SS⁡xT⁡x−S
17 6 16 mpteq12dv ⊢s=S∧t=T→x∈0..^s+t⟼ifx∈0..^ss⁡xt⁡x−s=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S
18 df-concat ⊢++=s∈V,t∈V⟼x∈0..^s+t⟼ifx∈0..^ss⁡xt⁡x−s
19 ovex ⊢0..^S+T∈V
20 19 mptex ⊢x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S∈V
21 17 18 20 ovmpoa ⊢S∈V∧T∈V→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S
22 1 2 21 syl2an ⊢S∈V∧T∈W→S++T=x∈0..^S+T⟼ifx∈0..^SS⁡xT⁡x−S