Step | Hyp | Ref
| Expression |
1 | | lenco 13429 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑆)) = (#‘𝑆)) |
2 | 1 | 3adant2 1073 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑆)) = (#‘𝑆)) |
3 | | lenco 13429 |
. . . . . . 7
⊢ ((𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑇)) = (#‘𝑇)) |
4 | 3 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑇)) = (#‘𝑇)) |
5 | 2, 4 | oveq12d 6567 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((#‘(𝐹 ∘ 𝑆)) + (#‘(𝐹 ∘ 𝑇))) = ((#‘𝑆) + (#‘𝑇))) |
6 | 5 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^((#‘(𝐹 ∘ 𝑆)) + (#‘(𝐹 ∘ 𝑇)))) = (0..^((#‘𝑆) + (#‘𝑇)))) |
7 | 6 | mpteq1d 4666 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((#‘(𝐹 ∘ 𝑆)) + (#‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆)))))) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))))) |
8 | 2 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(#‘(𝐹 ∘ 𝑆))) = (0..^(#‘𝑆))) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → (0..^(#‘(𝐹 ∘ 𝑆))) = (0..^(#‘𝑆))) |
10 | 9 | eleq2d 2673 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))) ↔ 𝑥 ∈ (0..^(#‘𝑆)))) |
11 | 10 | ifbid 4058 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(#‘𝑆)), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆)))))) |
12 | | wrdf 13165 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → 𝑆:(0..^(#‘𝑆))⟶𝐴) |
13 | 12 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑆:(0..^(#‘𝑆))⟶𝐴) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → 𝑆:(0..^(#‘𝑆))⟶𝐴) |
15 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑆:(0..^(#‘𝑆))⟶𝐴 → 𝑆 Fn (0..^(#‘𝑆))) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → 𝑆 Fn (0..^(#‘𝑆))) |
17 | | fvco2 6183 |
. . . . . . . 8
⊢ ((𝑆 Fn (0..^(#‘𝑆)) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = (𝐹‘(𝑆‘𝑥))) |
18 | 16, 17 | sylan 487 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = (𝐹‘(𝑆‘𝑥))) |
19 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^(#‘𝑆)) → if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) = (𝐹‘(𝑆‘𝑥))) |
20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) = (𝐹‘(𝑆‘𝑥))) |
21 | 18, 20 | eqtr4d 2647 |
. . . . . 6
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆)))))) |
22 | | wrdf 13165 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → 𝑇:(0..^(#‘𝑇))⟶𝐴) |
23 | 22 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑇:(0..^(#‘𝑇))⟶𝐴) |
24 | 23 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑇:(0..^(#‘𝑇))⟶𝐴) |
25 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑇:(0..^(#‘𝑇))⟶𝐴 → 𝑇 Fn (0..^(#‘𝑇))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑇 Fn (0..^(#‘𝑇))) |
27 | | lencl 13179 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Word 𝐴 → (#‘𝑆) ∈
ℕ0) |
28 | 27 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐴 → (#‘𝑆) ∈ ℤ) |
29 | 28 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘𝑆) ∈ ℤ) |
30 | | fzospliti 12369 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ∧ (#‘𝑆) ∈ ℤ) → (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) |
31 | 30 | ancoms 468 |
. . . . . . . . . . 11
⊢
(((#‘𝑆) ∈
ℤ ∧ 𝑥 ∈
(0..^((#‘𝑆) +
(#‘𝑇)))) →
(𝑥 ∈
(0..^(#‘𝑆)) ∨
𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) |
32 | 29, 31 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) |
33 | 32 | orcanai 950 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) |
34 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ Word 𝐴 → (#‘𝑇) ∈
ℕ0) |
35 | 34 | nn0zd 11356 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → (#‘𝑇) ∈ ℤ) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘𝑇) ∈ ℤ) |
37 | 36 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → (#‘𝑇) ∈ ℤ) |
38 | | fzosubel3 12396 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ∧ (#‘𝑇) ∈ ℤ) → (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) |
39 | 33, 37, 38 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) |
40 | | fvco2 6183 |
. . . . . . . 8
⊢ ((𝑇 Fn (0..^(#‘𝑇)) ∧ (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘𝑆))) = (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) |
41 | 26, 39, 40 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘𝑆))) = (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) |
42 | 2 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 − (#‘(𝐹 ∘ 𝑆))) = (𝑥 − (#‘𝑆))) |
43 | 42 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆)))) = ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘𝑆)))) |
44 | 43 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆)))) = ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘𝑆)))) |
45 | | iffalse 4045 |
. . . . . . . 8
⊢ (¬
𝑥 ∈
(0..^(#‘𝑆)) →
if(𝑥 ∈
(0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) = (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) |
46 | 45 | adantl 481 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) = (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) |
47 | 41, 44, 46 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆)))) = if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆)))))) |
48 | 21, 47 | ifeqda 4071 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → if(𝑥 ∈ (0..^(#‘𝑆)), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆)))))) |
49 | 11, 48 | eqtrd 2644 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆)))))) |
50 | 49 | mpteq2dva 4672 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆)))))) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))))) |
51 | 7, 50 | eqtr2d 2645 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆)))))) = (𝑥 ∈ (0..^((#‘(𝐹 ∘ 𝑆)) + (#‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))))) |
52 | 14 | ffvelrnda 6267 |
. . . 4
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆‘𝑥) ∈ 𝐴) |
53 | 24, 39 | ffvelrnd 6268 |
. . . 4
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) ∧ ¬ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑇‘(𝑥 − (#‘𝑆))) ∈ 𝐴) |
54 | 52, 53 | ifclda 4070 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))) ∈ 𝐴) |
55 | | ccatfval 13211 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))))) |
56 | 55 | 3adant3 1074 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))))) |
57 | | simp3 1056 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵) |
58 | 57 | feqmptd 6159 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦))) |
59 | | fveq2 6103 |
. . . 4
⊢ (𝑦 = if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))) → (𝐹‘𝑦) = (𝐹‘if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))))) |
60 | | fvif 6114 |
. . . 4
⊢ (𝐹‘if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆))))) = if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))) |
61 | 59, 60 | syl6eq 2660 |
. . 3
⊢ (𝑦 = if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))) → (𝐹‘𝑦) = if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆)))))) |
62 | 54, 56, 58, 61 | fmptco 6303 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (#‘𝑆))))))) |
63 | | ffun 5961 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
64 | 63 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → Fun 𝐹) |
65 | | simp1 1054 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑆 ∈ Word 𝐴) |
66 | | cofunexg 7023 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑆 ∈ Word 𝐴) → (𝐹 ∘ 𝑆) ∈ V) |
67 | 64, 65, 66 | syl2anc 691 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑆) ∈ V) |
68 | | simp2 1055 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑇 ∈ Word 𝐴) |
69 | | cofunexg 7023 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑇 ∈ Word 𝐴) → (𝐹 ∘ 𝑇) ∈ V) |
70 | 64, 68, 69 | syl2anc 691 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑇) ∈ V) |
71 | | ccatfval 13211 |
. . 3
⊢ (((𝐹 ∘ 𝑆) ∈ V ∧ (𝐹 ∘ 𝑇) ∈ V) → ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)) = (𝑥 ∈ (0..^((#‘(𝐹 ∘ 𝑆)) + (#‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))))) |
72 | 67, 70, 71 | syl2anc 691 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)) = (𝑥 ∈ (0..^((#‘(𝐹 ∘ 𝑆)) + (#‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(#‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (#‘(𝐹 ∘ 𝑆))))))) |
73 | 51, 62, 72 | 3eqtr4d 2654 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇))) |