Step | Hyp | Ref
| Expression |
1 | | ofccat.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ Word 𝑆) |
2 | | wrdf 13165 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ Word 𝑆 → 𝐸:(0..^(#‘𝐸))⟶𝑆) |
3 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐸:(0..^(#‘𝐸))⟶𝑆 → 𝐸 Fn (0..^(#‘𝐸))) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 Fn (0..^(#‘𝐸))) |
5 | | ofccat.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ Word 𝑇) |
6 | | wrdf 13165 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Word 𝑇 → 𝐺:(0..^(#‘𝐺))⟶𝑇) |
7 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐺:(0..^(#‘𝐺))⟶𝑇 → 𝐺 Fn (0..^(#‘𝐺))) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Fn (0..^(#‘𝐺))) |
9 | | ofccat.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘𝐸) = (#‘𝐺)) |
10 | 9 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0..^(#‘𝐸)) = (0..^(#‘𝐺))) |
11 | 10 | fneq2d 5896 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 Fn (0..^(#‘𝐸)) ↔ 𝐺 Fn (0..^(#‘𝐺)))) |
12 | 8, 11 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 Fn (0..^(#‘𝐸))) |
13 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(0..^(#‘𝐸))
∈ V |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^(#‘𝐸)) ∈ V) |
15 | | inidm 3784 |
. . . . . . . . . 10
⊢
((0..^(#‘𝐸))
∩ (0..^(#‘𝐸))) =
(0..^(#‘𝐸)) |
16 | 4, 12, 14, 14, 15 | offn 6806 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ∘𝑓 𝑅𝐺) Fn (0..^(#‘𝐸))) |
17 | | hashfn 13025 |
. . . . . . . . 9
⊢ ((𝐸 ∘𝑓
𝑅𝐺) Fn (0..^(#‘𝐸)) → (#‘(𝐸 ∘𝑓 𝑅𝐺)) = (#‘(0..^(#‘𝐸)))) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (#‘(𝐸 ∘𝑓
𝑅𝐺)) = (#‘(0..^(#‘𝐸)))) |
19 | | wrdfin 13178 |
. . . . . . . . . 10
⊢ (𝐸 ∈ Word 𝑆 → 𝐸 ∈ Fin) |
20 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝐸 ∈ Fin →
(#‘𝐸) ∈
ℕ0) |
21 | 1, 19, 20 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐸) ∈
ℕ0) |
22 | | hashfzo0 13077 |
. . . . . . . . 9
⊢
((#‘𝐸) ∈
ℕ0 → (#‘(0..^(#‘𝐸))) = (#‘𝐸)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(#‘(0..^(#‘𝐸)))
= (#‘𝐸)) |
24 | 18, 23 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐸 ∘𝑓
𝑅𝐺)) = (#‘𝐸)) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (#‘(𝐸 ∘𝑓 𝑅𝐺)) = (#‘𝐸)) |
26 | 25 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))) = (0..^(#‘𝐸))) |
27 | 26 | eleq2d 2673 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))) ↔ 𝑖 ∈ (0..^(#‘𝐸)))) |
28 | 4 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → 𝐸 Fn (0..^(#‘𝐸))) |
29 | 12 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → 𝐺 Fn (0..^(#‘𝐸))) |
30 | 13 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (0..^(#‘𝐸)) ∈ V) |
31 | 27 | biimpa 500 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → 𝑖 ∈ (0..^(#‘𝐸))) |
32 | | fnfvof 6809 |
. . . . 5
⊢ (((𝐸 Fn (0..^(#‘𝐸)) ∧ 𝐺 Fn (0..^(#‘𝐸))) ∧ ((0..^(#‘𝐸)) ∈ V ∧ 𝑖 ∈ (0..^(#‘𝐸)))) → ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖) = ((𝐸‘𝑖)𝑅(𝐺‘𝑖))) |
33 | 28, 29, 30, 31, 32 | syl22anc 1319 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖) = ((𝐸‘𝑖)𝑅(𝐺‘𝑖))) |
34 | 24 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (#‘(𝐸 ∘𝑓 𝑅𝐺)) = (#‘𝐸)) |
35 | 34 | oveq2d 6565 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺))) = (𝑖 − (#‘𝐸))) |
36 | 35 | fveq2d 6107 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺)))) = ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘𝐸)))) |
37 | | ofccat.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ Word 𝑆) |
38 | | wrdf 13165 |
. . . . . . . 8
⊢ (𝐹 ∈ Word 𝑆 → 𝐹:(0..^(#‘𝐹))⟶𝑆) |
39 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:(0..^(#‘𝐹))⟶𝑆 → 𝐹 Fn (0..^(#‘𝐹))) |
40 | 37, 38, 39 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn (0..^(#‘𝐹))) |
41 | 40 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → 𝐹 Fn (0..^(#‘𝐹))) |
42 | | ofccat.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝐻 ∈ Word 𝑇) |
43 | | wrdf 13165 |
. . . . . . . . 9
⊢ (𝐻 ∈ Word 𝑇 → 𝐻:(0..^(#‘𝐻))⟶𝑇) |
44 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐻:(0..^(#‘𝐻))⟶𝑇 → 𝐻 Fn (0..^(#‘𝐻))) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 Fn (0..^(#‘𝐻))) |
46 | | ofccat.6 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐹) = (#‘𝐻)) |
47 | 46 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(#‘𝐹)) = (0..^(#‘𝐻))) |
48 | 47 | fneq2d 5896 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 Fn (0..^(#‘𝐹)) ↔ 𝐻 Fn (0..^(#‘𝐻)))) |
49 | 45, 48 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → 𝐻 Fn (0..^(#‘𝐹))) |
50 | 49 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → 𝐻 Fn (0..^(#‘𝐹))) |
51 | | ovex 6577 |
. . . . . . 7
⊢
(0..^(#‘𝐹))
∈ V |
52 | 51 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (0..^(#‘𝐹)) ∈ V) |
53 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) |
54 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) |
55 | 26 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))) = (0..^(#‘𝐸))) |
56 | 54, 55 | neleqtrd 2709 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → ¬ 𝑖 ∈ (0..^(#‘𝐸))) |
57 | 21 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (#‘𝐸) ∈
ℕ0) |
58 | 57 | nn0zd 11356 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (#‘𝐸) ∈ ℤ) |
59 | | wrdfin 13178 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word 𝑆 → 𝐹 ∈ Fin) |
60 | | hashcl 13009 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℕ0) |
61 | 37, 59, 60 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐹) ∈
ℕ0) |
62 | 61 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (#‘𝐹) ∈
ℕ0) |
63 | 62 | nn0zd 11356 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (#‘𝐹) ∈ ℤ) |
64 | | fzocatel 12399 |
. . . . . . 7
⊢ (((𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ∧ ¬ 𝑖 ∈ (0..^(#‘𝐸))) ∧ ((#‘𝐸) ∈ ℤ ∧ (#‘𝐹) ∈ ℤ)) → (𝑖 − (#‘𝐸)) ∈ (0..^(#‘𝐹))) |
65 | 53, 56, 58, 63, 64 | syl22anc 1319 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → (𝑖 − (#‘𝐸)) ∈ (0..^(#‘𝐹))) |
66 | | fnfvof 6809 |
. . . . . 6
⊢ (((𝐹 Fn (0..^(#‘𝐹)) ∧ 𝐻 Fn (0..^(#‘𝐹))) ∧ ((0..^(#‘𝐹)) ∈ V ∧ (𝑖 − (#‘𝐸)) ∈ (0..^(#‘𝐹)))) → ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘𝐸))) = ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸))))) |
67 | 41, 50, 52, 65, 66 | syl22anc 1319 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘𝐸))) = ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸))))) |
68 | 36, 67 | eqtrd 2644 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) ∧ ¬ 𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺)))) → ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺)))) = ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸))))) |
69 | 27, 33, 68 | ifbieq12d2 4069 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺))))) = if(𝑖 ∈ (0..^(#‘𝐸)), ((𝐸‘𝑖)𝑅(𝐺‘𝑖)), ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸)))))) |
70 | 69 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺)))))) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐸)), ((𝐸‘𝑖)𝑅(𝐺‘𝑖)), ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸))))))) |
71 | | ovex 6577 |
. . . 4
⊢ (𝐸 ∘𝑓
𝑅𝐺) ∈ V |
72 | | ovex 6577 |
. . . 4
⊢ (𝐹 ∘𝑓
𝑅𝐻) ∈ V |
73 | | ccatfval 13211 |
. . . 4
⊢ (((𝐸 ∘𝑓
𝑅𝐺) ∈ V ∧ (𝐹 ∘𝑓 𝑅𝐻) ∈ V) → ((𝐸 ∘𝑓 𝑅𝐺) ++ (𝐹 ∘𝑓 𝑅𝐻)) = (𝑖 ∈ (0..^((#‘(𝐸 ∘𝑓 𝑅𝐺)) + (#‘(𝐹 ∘𝑓 𝑅𝐻)))) ↦ if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺))))))) |
74 | 71, 72, 73 | mp2an 704 |
. . 3
⊢ ((𝐸 ∘𝑓
𝑅𝐺) ++ (𝐹 ∘𝑓 𝑅𝐻)) = (𝑖 ∈ (0..^((#‘(𝐸 ∘𝑓 𝑅𝐺)) + (#‘(𝐹 ∘𝑓 𝑅𝐻)))) ↦ if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺)))))) |
75 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (0..^(#‘𝐹)) ∈ V) |
76 | | inidm 3784 |
. . . . . . . . 9
⊢
((0..^(#‘𝐹))
∩ (0..^(#‘𝐹))) =
(0..^(#‘𝐹)) |
77 | 40, 49, 75, 75, 76 | offn 6806 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐻) Fn (0..^(#‘𝐹))) |
78 | | hashfn 13025 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓
𝑅𝐻) Fn (0..^(#‘𝐹)) → (#‘(𝐹 ∘𝑓 𝑅𝐻)) = (#‘(0..^(#‘𝐹)))) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (#‘(𝐹 ∘𝑓
𝑅𝐻)) = (#‘(0..^(#‘𝐹)))) |
80 | | hashfzo0 13077 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ0 → (#‘(0..^(#‘𝐹))) = (#‘𝐹)) |
81 | 61, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(#‘(0..^(#‘𝐹)))
= (#‘𝐹)) |
82 | 79, 81 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (#‘(𝐹 ∘𝑓
𝑅𝐻)) = (#‘𝐹)) |
83 | 24, 82 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((#‘(𝐸 ∘𝑓
𝑅𝐺)) + (#‘(𝐹 ∘𝑓 𝑅𝐻))) = ((#‘𝐸) + (#‘𝐹))) |
84 | 83 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (0..^((#‘(𝐸 ∘𝑓
𝑅𝐺)) + (#‘(𝐹 ∘𝑓 𝑅𝐻)))) = (0..^((#‘𝐸) + (#‘𝐹)))) |
85 | 84 | mpteq1d 4666 |
. . 3
⊢ (𝜑 → (𝑖 ∈ (0..^((#‘(𝐸 ∘𝑓 𝑅𝐺)) + (#‘(𝐹 ∘𝑓 𝑅𝐻)))) ↦ if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺)))))) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺))))))) |
86 | 74, 85 | syl5eq 2656 |
. 2
⊢ (𝜑 → ((𝐸 ∘𝑓 𝑅𝐺) ++ (𝐹 ∘𝑓 𝑅𝐻)) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘(𝐸 ∘𝑓 𝑅𝐺))), ((𝐸 ∘𝑓 𝑅𝐺)‘𝑖), ((𝐹 ∘𝑓 𝑅𝐻)‘(𝑖 − (#‘(𝐸 ∘𝑓 𝑅𝐺))))))) |
87 | | ovex 6577 |
. . . . . 6
⊢
(0..^((#‘𝐸) +
(#‘𝐹))) ∈
V |
88 | 87 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^((#‘𝐸) + (#‘𝐹))) ∈ V) |
89 | | fvex 6113 |
. . . . . . 7
⊢ (𝐸‘𝑖) ∈ V |
90 | | fvex 6113 |
. . . . . . 7
⊢ (𝐹‘(𝑖 − (#‘𝐸))) ∈ V |
91 | 89, 90 | ifex 4106 |
. . . . . 6
⊢ if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸)))) ∈ V |
92 | 91 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸)))) ∈ V) |
93 | | fvex 6113 |
. . . . . . 7
⊢ (𝐺‘𝑖) ∈ V |
94 | | fvex 6113 |
. . . . . . 7
⊢ (𝐻‘(𝑖 − (#‘𝐺))) ∈ V |
95 | 93, 94 | ifex 4106 |
. . . . . 6
⊢ if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))) ∈ V |
96 | 95 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))) ∈ V) |
97 | | ccatfval 13211 |
. . . . . 6
⊢ ((𝐸 ∈ Word 𝑆 ∧ 𝐹 ∈ Word 𝑆) → (𝐸 ++ 𝐹) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸)))))) |
98 | 1, 37, 97 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐸 ++ 𝐹) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸)))))) |
99 | | ccatfval 13211 |
. . . . . . 7
⊢ ((𝐺 ∈ Word 𝑇 ∧ 𝐻 ∈ Word 𝑇) → (𝐺 ++ 𝐻) = (𝑖 ∈ (0..^((#‘𝐺) + (#‘𝐻))) ↦ if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))))) |
100 | 5, 42, 99 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐺 ++ 𝐻) = (𝑖 ∈ (0..^((#‘𝐺) + (#‘𝐻))) ↦ if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))))) |
101 | 9, 46 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐸) + (#‘𝐹)) = ((#‘𝐺) + (#‘𝐻))) |
102 | 101 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (0..^((#‘𝐸) + (#‘𝐹))) = (0..^((#‘𝐺) + (#‘𝐻)))) |
103 | 102 | mpteq1d 4666 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺))))) = (𝑖 ∈ (0..^((#‘𝐺) + (#‘𝐻))) ↦ if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))))) |
104 | 100, 103 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → (𝐺 ++ 𝐻) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))))) |
105 | 88, 92, 96, 98, 104 | offval2 6812 |
. . . 4
⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘𝑓 𝑅(𝐺 ++ 𝐻)) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺))))))) |
106 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (#‘𝐸) = (#‘𝐺)) |
107 | 106 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (0..^(#‘𝐸)) = (0..^(#‘𝐺))) |
108 | 107 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (𝑖 ∈ (0..^(#‘𝐸)) ↔ 𝑖 ∈ (0..^(#‘𝐺)))) |
109 | 106 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (𝑖 − (#‘𝐸)) = (𝑖 − (#‘𝐺))) |
110 | 109 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (𝐻‘(𝑖 − (#‘𝐸))) = (𝐻‘(𝑖 − (#‘𝐺)))) |
111 | 108, 110 | ifbieq2d 4061 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → if(𝑖 ∈ (0..^(#‘𝐸)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐸)))) = if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺))))) |
112 | 111 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹)))) → (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐸)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐸))))) = (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺)))))) |
113 | 112 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐸)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐸)))))) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐺)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐺))))))) |
114 | 105, 113 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘𝑓 𝑅(𝐺 ++ 𝐻)) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐸)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐸))))))) |
115 | | ovif12 6637 |
. . . 4
⊢ (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐸)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐸))))) = if(𝑖 ∈ (0..^(#‘𝐸)), ((𝐸‘𝑖)𝑅(𝐺‘𝑖)), ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸))))) |
116 | 115 | mpteq2i 4669 |
. . 3
⊢ (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ (if(𝑖 ∈ (0..^(#‘𝐸)), (𝐸‘𝑖), (𝐹‘(𝑖 − (#‘𝐸))))𝑅if(𝑖 ∈ (0..^(#‘𝐸)), (𝐺‘𝑖), (𝐻‘(𝑖 − (#‘𝐸)))))) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐸)), ((𝐸‘𝑖)𝑅(𝐺‘𝑖)), ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸)))))) |
117 | 114, 116 | syl6eq 2660 |
. 2
⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘𝑓 𝑅(𝐺 ++ 𝐻)) = (𝑖 ∈ (0..^((#‘𝐸) + (#‘𝐹))) ↦ if(𝑖 ∈ (0..^(#‘𝐸)), ((𝐸‘𝑖)𝑅(𝐺‘𝑖)), ((𝐹‘(𝑖 − (#‘𝐸)))𝑅(𝐻‘(𝑖 − (#‘𝐸))))))) |
118 | 70, 86, 117 | 3eqtr4rd 2655 |
1
⊢ (𝜑 → ((𝐸 ++ 𝐹) ∘𝑓 𝑅(𝐺 ++ 𝐻)) = ((𝐸 ∘𝑓 𝑅𝐺) ++ (𝐹 ∘𝑓 𝑅𝐻))) |