Metamath Proof Explorer

Theorem ccatfval

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

Ref Expression
Assertion ccatfval 
|- ( ( S e. V /\ T e. W ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( S e. V -> S e. _V )
2 elex 
 |-  ( T e. W -> T e. _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 e. ( 0 ..^ ( # ` s ) ) <-> x e. ( 0 ..^ ( # ` S ) ) ) )
9 8 adantr 
 |-  ( ( s = S /\ t = T ) -> ( x e. ( 0 ..^ ( # ` s ) ) <-> x e. ( 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 e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) )
17 6 16 mpteq12dv 
 |-  ( ( s = S /\ t = T ) -> ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
18 df-concat 
 |-  ++ = ( s e. _V , t e. _V |-> ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) )
19 ovex 
 |-  ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) e. _V
20 19 mptex 
 |-  ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) e. _V
21 17 18 20 ovmpoa 
 |-  ( ( S e. _V /\ T e. _V ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
22 1 2 21 syl2an 
 |-  ( ( S e. V /\ T e. W ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )