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 ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ 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 → if x ∈ 0 ..^ s s ⁡ x t ⁡ x − s = if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
17 6 16 mpteq12dv ⊢ s = S ∧ t = T → x ∈ 0 ..^ s + t ⟼ if x ∈ 0 ..^ s s ⁡ x t ⁡ x − s = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
18 df-concat ⊢ ++ = s ∈ V , t ∈ V ⟼ x ∈ 0 ..^ s + t ⟼ if x ∈ 0 ..^ s s ⁡ x t ⁡ x − s
19 ovex ⊢ 0 ..^ S + T ∈ V
20 19 mptex ⊢ x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S ∈ V
21 17 18 20 ovmpoa ⊢ S ∈ V ∧ T ∈ V → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S
22 1 2 21 syl2an ⊢ S ∈ V ∧ T ∈ W → S ++ T = x ∈ 0 ..^ S + T ⟼ if x ∈ 0 ..^ S S ⁡ x T ⁡ x − S