Metamath Proof Explorer


Theorem ccatco

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

Ref Expression
Assertion ccatco ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝐹 ∘ ( 𝑆 ++ 𝑇 ) ) = ( ( 𝐹𝑆 ) ++ ( 𝐹𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 lenco ( ( 𝑆 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ♯ ‘ ( 𝐹𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
2 1 3adant2 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ♯ ‘ ( 𝐹𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
3 lenco ( ( 𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ♯ ‘ ( 𝐹𝑇 ) ) = ( ♯ ‘ 𝑇 ) )
4 3 3adant1 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ♯ ‘ ( 𝐹𝑇 ) ) = ( ♯ ‘ 𝑇 ) )
5 2 4 oveq12d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ( ♯ ‘ ( 𝐹𝑆 ) ) + ( ♯ ‘ ( 𝐹𝑇 ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
6 5 oveq2d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 0 ..^ ( ( ♯ ‘ ( 𝐹𝑆 ) ) + ( ♯ ‘ ( 𝐹𝑇 ) ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
7 6 mpteq1d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐹𝑆 ) ) + ( ♯ ‘ ( 𝐹𝑇 ) ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) ) )
8 2 oveq2d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
9 8 adantr ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
10 9 eleq2d ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) ↔ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
11 10 ifbid ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) )
12 wrdf ( 𝑆 ∈ Word 𝐴𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
13 12 3ad2ant1 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
14 13 adantr ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ 𝐴 )
15 14 ffnd ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
16 fvco2 ( ( 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝐹𝑆 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑆𝑥 ) ) )
17 15 16 sylan ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝐹𝑆 ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑆𝑥 ) ) )
18 iftrue ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑆𝑥 ) ) )
19 18 adantl ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑆𝑥 ) ) )
20 17 19 eqtr4d ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝐹𝑆 ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
21 wrdf ( 𝑇 ∈ Word 𝐴𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐴 )
22 21 3ad2ant2 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐴 )
23 22 ad2antrr ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐴 )
24 23 ffnd ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
25 lencl ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
26 25 nn0zd ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ℤ )
27 26 3ad2ant1 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ℤ )
28 fzospliti ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
29 28 ancoms ( ( ( ♯ ‘ 𝑆 ) ∈ ℤ ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
30 27 29 sylan ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
31 30 orcanai ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
32 lencl ( 𝑇 ∈ Word 𝐴 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
33 32 nn0zd ( 𝑇 ∈ Word 𝐴 → ( ♯ ‘ 𝑇 ) ∈ ℤ )
34 33 3ad2ant2 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ♯ ‘ 𝑇 ) ∈ ℤ )
35 34 ad2antrr ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ 𝑇 ) ∈ ℤ )
36 fzosubel3 ( ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
37 31 35 36 syl2anc ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
38 fvco2 ( ( 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
39 24 37 38 syl2anc ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) = ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
40 2 oveq2d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) = ( 𝑥 − ( ♯ ‘ 𝑆 ) ) )
41 40 fveq2d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) = ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
42 41 ad2antrr ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) = ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
43 iffalse ( ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
44 43 adantl ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) = ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
45 39 42 44 3eqtr4d ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
46 20 45 ifeqda ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
47 11 46 eqtrd ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
48 47 mpteq2dva ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) )
49 7 48 eqtr2d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐹𝑆 ) ) + ( ♯ ‘ ( 𝐹𝑇 ) ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) ) )
50 14 ffvelrnda ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆𝑥 ) ∈ 𝐴 )
51 23 37 ffvelrnd ( ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ ¬ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ∈ 𝐴 )
52 50 51 ifclda ( ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ∈ 𝐴 )
53 ccatfval ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
54 53 3adant3 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
55 simp3 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → 𝐹 : 𝐴𝐵 )
56 55 feqmptd ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → 𝐹 = ( 𝑦𝐴 ↦ ( 𝐹𝑦 ) ) )
57 fveq2 ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝐹𝑦 ) = ( 𝐹 ‘ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
58 fvif ( 𝐹 ‘ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
59 57 58 eqtrdi ( 𝑦 = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) → ( 𝐹𝑦 ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
60 52 54 56 59 fmptco ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝐹 ∘ ( 𝑆 ++ 𝑇 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝐹 ‘ ( 𝑆𝑥 ) ) , ( 𝐹 ‘ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) )
61 ffun ( 𝐹 : 𝐴𝐵 → Fun 𝐹 )
62 61 3ad2ant3 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → Fun 𝐹 )
63 simp1 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → 𝑆 ∈ Word 𝐴 )
64 cofunexg ( ( Fun 𝐹𝑆 ∈ Word 𝐴 ) → ( 𝐹𝑆 ) ∈ V )
65 62 63 64 syl2anc ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝐹𝑆 ) ∈ V )
66 simp2 ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → 𝑇 ∈ Word 𝐴 )
67 cofunexg ( ( Fun 𝐹𝑇 ∈ Word 𝐴 ) → ( 𝐹𝑇 ) ∈ V )
68 62 66 67 syl2anc ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝐹𝑇 ) ∈ V )
69 ccatfval ( ( ( 𝐹𝑆 ) ∈ V ∧ ( 𝐹𝑇 ) ∈ V ) → ( ( 𝐹𝑆 ) ++ ( 𝐹𝑇 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐹𝑆 ) ) + ( ♯ ‘ ( 𝐹𝑇 ) ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) ) )
70 65 68 69 syl2anc ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( ( 𝐹𝑆 ) ++ ( 𝐹𝑇 ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐹𝑆 ) ) + ( ♯ ‘ ( 𝐹𝑇 ) ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹𝑆 ) ) ) , ( ( 𝐹𝑆 ) ‘ 𝑥 ) , ( ( 𝐹𝑇 ) ‘ ( 𝑥 − ( ♯ ‘ ( 𝐹𝑆 ) ) ) ) ) ) )
71 49 60 70 3eqtr4d ( ( 𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴𝐹 : 𝐴𝐵 ) → ( 𝐹 ∘ ( 𝑆 ++ 𝑇 ) ) = ( ( 𝐹𝑆 ) ++ ( 𝐹𝑇 ) ) )