Step | Hyp | Ref
| Expression |
1 | | lenco 13798 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑆)) = (♯‘𝑆)) |
2 | 1 | 3adant2 1126 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑆)) = (♯‘𝑆)) |
3 | | lenco 13798 |
. . . . . . 7
⊢ ((𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑇)) = (♯‘𝑇)) |
4 | 3 | 3adant1 1125 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑇)) = (♯‘𝑇)) |
5 | 2, 4 | oveq12d 6832 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇))) = ((♯‘𝑆) + (♯‘𝑇))) |
6 | 5 | oveq2d 6830 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) = (0..^((♯‘𝑆) + (♯‘𝑇)))) |
7 | 6 | mpteq1d 4890 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘(𝐹
∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))))) |
8 | 2 | oveq2d 6830 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (0..^(♯‘(𝐹 ∘ 𝑆))) = (0..^(♯‘𝑆))) |
9 | 8 | adantr 472 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) →
(0..^(♯‘(𝐹
∘ 𝑆))) =
(0..^(♯‘𝑆))) |
10 | 9 | eleq2d 2825 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))) ↔ 𝑥 ∈ (0..^(♯‘𝑆)))) |
11 | 10 | ifbid 4252 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈
(0..^(♯‘(𝐹
∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))) |
12 | | wrdf 13516 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐴 → 𝑆:(0..^(♯‘𝑆))⟶𝐴) |
13 | 12 | 3ad2ant1 1128 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑆:(0..^(♯‘𝑆))⟶𝐴) |
14 | 13 | adantr 472 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑆:(0..^(♯‘𝑆))⟶𝐴) |
15 | | ffn 6206 |
. . . . . . . . 9
⊢ (𝑆:(0..^(♯‘𝑆))⟶𝐴 → 𝑆 Fn (0..^(♯‘𝑆))) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑆 Fn (0..^(♯‘𝑆))) |
17 | | fvco2 6436 |
. . . . . . . 8
⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = (𝐹‘(𝑆‘𝑥))) |
18 | 16, 17 | sylan 489 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = (𝐹‘(𝑆‘𝑥))) |
19 | | iftrue 4236 |
. . . . . . . 8
⊢ (𝑥 ∈
(0..^(♯‘𝑆))
→ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑆‘𝑥))) |
20 | 19 | adantl 473 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑆‘𝑥))) |
21 | 18, 20 | eqtr4d 2797 |
. . . . . 6
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝐹 ∘ 𝑆)‘𝑥) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) |
22 | | wrdf 13516 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → 𝑇:(0..^(♯‘𝑇))⟶𝐴) |
23 | 22 | 3ad2ant2 1129 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑇:(0..^(♯‘𝑇))⟶𝐴) |
24 | 23 | ad2antrr 764 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ 𝑇:(0..^(♯‘𝑇))⟶𝐴) |
25 | | ffn 6206 |
. . . . . . . . 9
⊢ (𝑇:(0..^(♯‘𝑇))⟶𝐴 → 𝑇 Fn (0..^(♯‘𝑇))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ 𝑇 Fn
(0..^(♯‘𝑇))) |
27 | | lencl 13530 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈
ℕ0) |
28 | 27 | nn0zd 11692 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℤ) |
29 | 28 | 3ad2ant1 1128 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘𝑆) ∈ ℤ) |
30 | | fzospliti 12714 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
(0..^((♯‘𝑆) +
(♯‘𝑇))) ∧
(♯‘𝑆) ∈
ℤ) → (𝑥 ∈
(0..^(♯‘𝑆))
∨ 𝑥 ∈
((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) |
31 | 30 | ancoms 468 |
. . . . . . . . . . 11
⊢
(((♯‘𝑆)
∈ ℤ ∧ 𝑥
∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) |
32 | 29, 31 | sylan 489 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) |
33 | 32 | orcanai 990 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ 𝑥 ∈
((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) |
34 | | lencl 13530 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈
ℕ0) |
35 | 34 | nn0zd 11692 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℤ) |
36 | 35 | 3ad2ant2 1129 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘𝑇) ∈ ℤ) |
37 | 36 | ad2antrr 764 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ (♯‘𝑇)
∈ ℤ) |
38 | | fzosubel3 12743 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) ∧ (♯‘𝑇) ∈ ℤ) → (𝑥 − (♯‘𝑆)) ∈
(0..^(♯‘𝑇))) |
39 | 33, 37, 38 | syl2anc 696 |
. . . . . . . 8
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ (𝑥 −
(♯‘𝑆)) ∈
(0..^(♯‘𝑇))) |
40 | | fvco2 6436 |
. . . . . . . 8
⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) |
41 | 26, 39, 40 | syl2anc 696 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) |
42 | 2 | oveq2d 6830 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 − (♯‘(𝐹 ∘ 𝑆))) = (𝑥 − (♯‘𝑆))) |
43 | 42 | fveq2d 6357 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))) = ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆)))) |
44 | 43 | ad2antrr 764 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))) = ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘𝑆)))) |
45 | | iffalse 4239 |
. . . . . . . 8
⊢ (¬
𝑥 ∈
(0..^(♯‘𝑆))
→ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) |
46 | 45 | adantl 473 |
. . . . . . 7
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) = (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) |
47 | 41, 44, 46 | 3eqtr4d 2804 |
. . . . . 6
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) |
48 | 21, 47 | ifeqda 4265 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈
(0..^(♯‘𝑆)),
((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) |
49 | 11, 48 | eqtrd 2794 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈
(0..^(♯‘(𝐹
∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) |
50 | 49 | mpteq2dva 4896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘(𝐹
∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆)))))) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))) |
51 | 7, 50 | eqtr2d 2795 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) = (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))))) |
52 | 14 | ffvelrnda 6523 |
. . . 4
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ 𝐴) |
53 | 24, 39 | ffvelrnd 6524 |
. . . 4
⊢ ((((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) ∧ ¬ 𝑥 ∈
(0..^(♯‘𝑆)))
→ (𝑇‘(𝑥 − (♯‘𝑆))) ∈ 𝐴) |
54 | 52, 53 | ifclda 4264 |
. . 3
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))) ∈ 𝐴) |
55 | | ccatfval 13565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))))) |
56 | 55 | 3adant3 1127 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))))) |
57 | | simp3 1133 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹:𝐴⟶𝐵) |
58 | 57 | feqmptd 6412 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝐹‘𝑦))) |
59 | | fveq2 6353 |
. . . 4
⊢ (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))) → (𝐹‘𝑦) = (𝐹‘if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))))) |
60 | | fvif 6366 |
. . . 4
⊢ (𝐹‘if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))) |
61 | 59, 60 | syl6eq 2810 |
. . 3
⊢ (𝑦 = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))) → (𝐹‘𝑦) = if(𝑥 ∈ (0..^(♯‘𝑆)), (𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆)))))) |
62 | 54, 56, 58, 61 | fmptco 6560 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈
(0..^(♯‘𝑆)),
(𝐹‘(𝑆‘𝑥)), (𝐹‘(𝑇‘(𝑥 − (♯‘𝑆))))))) |
63 | | ffun 6209 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
64 | 63 | 3ad2ant3 1130 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → Fun 𝐹) |
65 | | simp1 1131 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑆 ∈ Word 𝐴) |
66 | | cofunexg 7296 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑆 ∈ Word 𝐴) → (𝐹 ∘ 𝑆) ∈ V) |
67 | 64, 65, 66 | syl2anc 696 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑆) ∈ V) |
68 | | simp2 1132 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → 𝑇 ∈ Word 𝐴) |
69 | | cofunexg 7296 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑇 ∈ Word 𝐴) → (𝐹 ∘ 𝑇) ∈ V) |
70 | 64, 68, 69 | syl2anc 696 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑇) ∈ V) |
71 | | ccatfval 13565 |
. . 3
⊢ (((𝐹 ∘ 𝑆) ∈ V ∧ (𝐹 ∘ 𝑇) ∈ V) → ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)) = (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))))) |
72 | 67, 70, 71 | syl2anc 696 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)) = (𝑥 ∈ (0..^((♯‘(𝐹 ∘ 𝑆)) + (♯‘(𝐹 ∘ 𝑇)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝐹 ∘ 𝑆))), ((𝐹 ∘ 𝑆)‘𝑥), ((𝐹 ∘ 𝑇)‘(𝑥 − (♯‘(𝐹 ∘ 𝑆))))))) |
73 | 51, 62, 72 | 3eqtr4d 2804 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇))) |