Metamath Proof Explorer

Theorem ccatco

Description: Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion ccatco 
|- ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( F o. ( S ++ T ) ) = ( ( F o. S ) ++ ( F o. T ) ) )

Proof

Step Hyp Ref Expression
1 lenco 
 |-  ( ( S e. Word A /\ F : A --> B ) -> ( # ` ( F o. S ) ) = ( # ` S ) )
2 1 3adant2 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( # ` ( F o. S ) ) = ( # ` S ) )
3 lenco 
 |-  ( ( T e. Word A /\ F : A --> B ) -> ( # ` ( F o. T ) ) = ( # ` T ) )
4 3 3adant1 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( # ` ( F o. T ) ) = ( # ` T ) )
5 2 4 oveq12d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( ( # ` ( F o. S ) ) + ( # ` ( F o. T ) ) ) = ( ( # ` S ) + ( # ` T ) ) )
6 5 oveq2d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( 0 ..^ ( ( # ` ( F o. S ) ) + ( # ` ( F o. T ) ) ) ) = ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
7 6 mpteq1d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( ( # ` ( F o. S ) ) + ( # ` ( F o. T ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) ) )
8 2 oveq2d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( 0 ..^ ( # ` ( F o. S ) ) ) = ( 0 ..^ ( # ` S ) ) )
9 8 adantr 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( 0 ..^ ( # ` ( F o. S ) ) ) = ( 0 ..^ ( # ` S ) ) )
10 9 eleq2d 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) <-> x e. ( 0 ..^ ( # ` S ) ) ) )
11 10 ifbid 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) )
12 wrdf 
 |-  ( S e. Word A -> S : ( 0 ..^ ( # ` S ) ) --> A )
13 12 3ad2ant1 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> S : ( 0 ..^ ( # ` S ) ) --> A )
14 13 adantr 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> S : ( 0 ..^ ( # ` S ) ) --> A )
15 14 ffnd 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> S Fn ( 0 ..^ ( # ` S ) ) )
16 fvco2 
 |-  ( ( S Fn ( 0 ..^ ( # ` S ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( F o. S ) ` x ) = ( F ` ( S ` x ) ) )
17 15 16 sylan 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( F o. S ) ` x ) = ( F ` ( S ` x ) ) )
18 iftrue 
 |-  ( x e. ( 0 ..^ ( # ` S ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) = ( F ` ( S ` x ) ) )
19 18 adantl 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) = ( F ` ( S ` x ) ) )
20 17 19 eqtr4d 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( F o. S ) ` x ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) )
21 wrdf 
 |-  ( T e. Word A -> T : ( 0 ..^ ( # ` T ) ) --> A )
22 21 3ad2ant2 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> T : ( 0 ..^ ( # ` T ) ) --> A )
23 22 ad2antrr 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> T : ( 0 ..^ ( # ` T ) ) --> A )
24 23 ffnd 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> T Fn ( 0 ..^ ( # ` T ) ) )
25 lencl 
 |-  ( S e. Word A -> ( # ` S ) e. NN0 )
26 25 nn0zd 
 |-  ( S e. Word A -> ( # ` S ) e. ZZ )
27 26 3ad2ant1 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( # ` S ) e. ZZ )
28 fzospliti 
 |-  ( ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) /\ ( # ` S ) e. ZZ ) -> ( x e. ( 0 ..^ ( # ` S ) ) \/ x e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) )
29 28 ancoms 
 |-  ( ( ( # ` S ) e. ZZ /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( x e. ( 0 ..^ ( # ` S ) ) \/ x e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) )
30 27 29 sylan 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( x e. ( 0 ..^ ( # ` S ) ) \/ x e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) )
31 30 orcanai 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> x e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) )
32 lencl 
 |-  ( T e. Word A -> ( # ` T ) e. NN0 )
33 32 nn0zd 
 |-  ( T e. Word A -> ( # ` T ) e. ZZ )
34 33 3ad2ant2 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( # ` T ) e. ZZ )
35 34 ad2antrr 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( # ` T ) e. ZZ )
36 fzosubel3 
 |-  ( ( x e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) /\ ( # ` T ) e. ZZ ) -> ( x - ( # ` S ) ) e. ( 0 ..^ ( # ` T ) ) )
37 31 35 36 syl2anc 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( x - ( # ` S ) ) e. ( 0 ..^ ( # ` T ) ) )
38 fvco2 
 |-  ( ( T Fn ( 0 ..^ ( # ` T ) ) /\ ( x - ( # ` S ) ) e. ( 0 ..^ ( # ` T ) ) ) -> ( ( F o. T ) ` ( x - ( # ` S ) ) ) = ( F ` ( T ` ( x - ( # ` S ) ) ) ) )
39 24 37 38 syl2anc 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( F o. T ) ` ( x - ( # ` S ) ) ) = ( F ` ( T ` ( x - ( # ` S ) ) ) ) )
40 2 oveq2d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( x - ( # ` ( F o. S ) ) ) = ( x - ( # ` S ) ) )
41 40 fveq2d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) = ( ( F o. T ) ` ( x - ( # ` S ) ) ) )
42 41 ad2antrr 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) = ( ( F o. T ) ` ( x - ( # ` S ) ) ) )
43 iffalse 
 |-  ( -. x e. ( 0 ..^ ( # ` S ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) = ( F ` ( T ` ( x - ( # ` S ) ) ) ) )
44 43 adantl 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) = ( F ` ( T ` ( x - ( # ` S ) ) ) ) )
45 39 42 44 3eqtr4d 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) )
46 20 45 ifeqda 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) )
47 11 46 eqtrd 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) )
48 47 mpteq2dva 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) ) )
49 7 48 eqtr2d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` ( F o. S ) ) + ( # ` ( F o. T ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) ) )
50 14 ffvelrnda 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( S ` x ) e. A )
51 23 37 ffvelrnd 
 |-  ( ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( T ` ( x - ( # ` S ) ) ) e. A )
52 50 51 ifclda 
 |-  ( ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) e. A )
53 ccatfval 
 |-  ( ( S e. Word A /\ T e. Word A ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
54 53 3adant3 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
55 simp3 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> F : A --> B )
56 55 feqmptd 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> F = ( y e. A |-> ( F ` y ) ) )
57 fveq2 
 |-  ( y = if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) -> ( F ` y ) = ( F ` if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
58 fvif 
 |-  ( F ` if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) )
59 57 58 eqtrdi 
 |-  ( y = if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) -> ( F ` y ) = if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) )
60 52 54 56 59 fmptco 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( F o. ( S ++ T ) ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( F ` ( S ` x ) ) , ( F ` ( T ` ( x - ( # ` S ) ) ) ) ) ) )
61 ffun 
 |-  ( F : A --> B -> Fun F )
62 61 3ad2ant3 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> Fun F )
63 simp1 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> S e. Word A )
64 cofunexg 
 |-  ( ( Fun F /\ S e. Word A ) -> ( F o. S ) e. _V )
65 62 63 64 syl2anc 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( F o. S ) e. _V )
66 simp2 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> T e. Word A )
67 cofunexg 
 |-  ( ( Fun F /\ T e. Word A ) -> ( F o. T ) e. _V )
68 62 66 67 syl2anc 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( F o. T ) e. _V )
69 ccatfval 
 |-  ( ( ( F o. S ) e. _V /\ ( F o. T ) e. _V ) -> ( ( F o. S ) ++ ( F o. T ) ) = ( x e. ( 0 ..^ ( ( # ` ( F o. S ) ) + ( # ` ( F o. T ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) ) )
70 65 68 69 syl2anc 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( ( F o. S ) ++ ( F o. T ) ) = ( x e. ( 0 ..^ ( ( # ` ( F o. S ) ) + ( # ` ( F o. T ) ) ) ) |-> if ( x e. ( 0 ..^ ( # ` ( F o. S ) ) ) , ( ( F o. S ) ` x ) , ( ( F o. T ) ` ( x - ( # ` ( F o. S ) ) ) ) ) ) )
71 49 60 70 3eqtr4d 
 |-  ( ( S e. Word A /\ T e. Word A /\ F : A --> B ) -> ( F o. ( S ++ T ) ) = ( ( F o. S ) ++ ( F o. T ) ) )