This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ 𝐴 )
51 23 37 ffvelcdmd ⊢ ( ( ( ( 𝑆 ∈ 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 𝐴 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ ( 𝑆 ++ 𝑇 ) ) = ( ( 𝐹 ∘ 𝑆 ) ++ ( 𝐹 ∘ 𝑇 ) ) )