Step | Hyp | Ref
| Expression |
1 | | ccatfval 13211 |
. . . 4
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (𝐴 ++ 𝐵) = (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) |
2 | 1 | eleq1d 2672 |
. . 3
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ∈ Word 𝑆)) |
3 | | wrdf 13165 |
. . . 4
⊢ ((𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ∈ Word 𝑆 → (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))):(0..^(#‘(𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))))⟶𝑆) |
4 | | funmpt 5840 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) |
5 | | fzofi 12635 |
. . . . . . . . . . 11
⊢
(0..^((#‘𝐴) +
(#‘𝐵))) ∈
Fin |
6 | | mptfi 8148 |
. . . . . . . . . . 11
⊢
((0..^((#‘𝐴) +
(#‘𝐵))) ∈ Fin
→ (𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ∈ Fin) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ∈ Fin |
8 | | hashfun 13084 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ∈ Fin → (Fun (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ↔ (#‘(𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) = (#‘dom (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))))) |
9 | 7, 8 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → (Fun
(𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ↔ (#‘(𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) = (#‘dom (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))))) |
10 | 4, 9 | mpbii 222 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘(𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) = (#‘dom (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))))) |
11 | | dmmptg 5549 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ V → dom (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) = (0..^((#‘𝐴) + (#‘𝐵)))) |
12 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐴‘𝑥) ∈ V |
13 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐵‘(𝑥 − (#‘𝐴))) ∈ V |
14 | 12, 13 | ifex 4106 |
. . . . . . . . . . . 12
⊢ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ V |
15 | 14 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) → if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ V) |
16 | 11, 15 | mprg 2910 |
. . . . . . . . . 10
⊢ dom
(𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) = (0..^((#‘𝐴) + (#‘𝐵))) |
17 | 16 | fveq2i 6106 |
. . . . . . . . 9
⊢
(#‘dom (𝑥
∈ (0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) = (#‘(0..^((#‘𝐴) + (#‘𝐵)))) |
18 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word V →
(#‘𝐴) ∈
ℕ0) |
19 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ Word V →
(#‘𝐵) ∈
ℕ0) |
20 | | nn0addcl 11205 |
. . . . . . . . . . 11
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐴) +
(#‘𝐵)) ∈
ℕ0) |
21 | 18, 19, 20 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
((#‘𝐴) +
(#‘𝐵)) ∈
ℕ0) |
22 | | hashfzo0 13077 |
. . . . . . . . . 10
⊢
(((#‘𝐴) +
(#‘𝐵)) ∈
ℕ0 → (#‘(0..^((#‘𝐴) + (#‘𝐵)))) = ((#‘𝐴) + (#‘𝐵))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘(0..^((#‘𝐴)
+ (#‘𝐵)))) =
((#‘𝐴) +
(#‘𝐵))) |
24 | 17, 23 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘dom (𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) = ((#‘𝐴) + (#‘𝐵))) |
25 | 10, 24 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘(𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))) = ((#‘𝐴) + (#‘𝐵))) |
26 | 25 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(0..^(#‘(𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵))) ↦
if(𝑥 ∈
(0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))))) = (0..^((#‘𝐴) + (#‘𝐵)))) |
27 | 26 | feq2d 5944 |
. . . . 5
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))):(0..^(#‘(𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))))⟶𝑆 ↔ (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))):(0..^((#‘𝐴) + (#‘𝐵)))⟶𝑆)) |
28 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) = (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) |
29 | 28 | fmpt 6289 |
. . . . . 6
⊢
(∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 ↔ (𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))):(0..^((#‘𝐴) + (#‘𝐵)))⟶𝑆) |
30 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐴 ∈ Word V) |
31 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℂ) |
32 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐵) ∈
ℕ0 → (#‘𝐵) ∈ ℂ) |
33 | | addcom 10101 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐴) ∈
ℂ ∧ (#‘𝐵)
∈ ℂ) → ((#‘𝐴) + (#‘𝐵)) = ((#‘𝐵) + (#‘𝐴))) |
34 | 31, 32, 33 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐴) +
(#‘𝐵)) =
((#‘𝐵) +
(#‘𝐴))) |
35 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℤ) |
36 | 35 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐴) ∈ ℤ
∧ (#‘𝐵) ∈
ℕ0)) |
37 | 36 | ancomd 466 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐵) ∈
ℕ0 ∧ (#‘𝐴) ∈ ℤ)) |
38 | | nn0pzuz 11621 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐵) ∈
ℕ0 ∧ (#‘𝐴) ∈ ℤ) → ((#‘𝐵) + (#‘𝐴)) ∈
(ℤ≥‘(#‘𝐴))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐵) +
(#‘𝐴)) ∈
(ℤ≥‘(#‘𝐴))) |
40 | 34, 39 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
((#‘𝐴) +
(#‘𝐵)) ∈
(ℤ≥‘(#‘𝐴))) |
41 | 18, 19, 40 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
((#‘𝐴) +
(#‘𝐵)) ∈
(ℤ≥‘(#‘𝐴))) |
42 | | fzoss2 12365 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐴) +
(#‘𝐵)) ∈
(ℤ≥‘(#‘𝐴)) → (0..^(#‘𝐴)) ⊆ (0..^((#‘𝐴) + (#‘𝐵)))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(0..^(#‘𝐴)) ⊆
(0..^((#‘𝐴) +
(#‘𝐵)))) |
44 | 43 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐴))) → 𝑦 ∈ (0..^((#‘𝐴) + (#‘𝐵)))) |
45 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (0..^(#‘𝐴)) ↔ 𝑦 ∈ (0..^(#‘𝐴)))) |
46 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐴‘𝑥) = (𝐴‘𝑦)) |
47 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 − (#‘𝐴)) = (𝑦 − (#‘𝐴))) |
48 | 47 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝐵‘(𝑥 − (#‘𝐴))) = (𝐵‘(𝑦 − (#‘𝐴)))) |
49 | 45, 46, 48 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) = if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴))))) |
50 | 49 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 ↔ if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴)))) ∈ 𝑆)) |
51 | 50 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0..^((#‘𝐴) + (#‘𝐵))) → (∀𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴)))) ∈ 𝑆)) |
52 | 44, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐴))) → (∀𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴)))) ∈ 𝑆)) |
53 | | iftrue 4042 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0..^(#‘𝐴)) → if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴)))) = (𝐴‘𝑦)) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐴))) → if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴)))) = (𝐴‘𝑦)) |
55 | 54 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐴))) → (if(𝑦 ∈ (0..^(#‘𝐴)), (𝐴‘𝑦), (𝐵‘(𝑦 − (#‘𝐴)))) ∈ 𝑆 ↔ (𝐴‘𝑦) ∈ 𝑆)) |
56 | 52, 55 | sylibd 228 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐴))) → (∀𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → (𝐴‘𝑦) ∈ 𝑆)) |
57 | 56 | impancom 455 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(#‘𝐴)) → (𝐴‘𝑦) ∈ 𝑆)) |
58 | 57 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) ∧ 𝑦 ∈ (0..^(#‘𝐴))) → (𝐴‘𝑦) ∈ 𝑆) |
59 | 58 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(#‘𝐴))(𝐴‘𝑦) ∈ 𝑆) |
60 | | iswrdsymb 13177 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧
∀𝑦 ∈
(0..^(#‘𝐴))(𝐴‘𝑦) ∈ 𝑆) → 𝐴 ∈ Word 𝑆) |
61 | 30, 59, 60 | syl2an2r 872 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → 𝐴 ∈ Word 𝑆) |
62 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → 𝐵 ∈ Word V) |
63 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → 𝑦 ∈ (0..^(#‘𝐵))) |
64 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘𝐴) ∈
ℕ0) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (#‘𝐴) ∈
ℕ0) |
66 | | elincfzoext 12393 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (0..^(#‘𝐵)) ∧ (#‘𝐴) ∈ ℕ0)
→ (𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐵) + (#‘𝐴)))) |
67 | 63, 65, 66 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐵) + (#‘𝐴)))) |
68 | 18 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Word V →
(#‘𝐴) ∈
ℂ) |
69 | 19 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Word V →
(#‘𝐵) ∈
ℂ) |
70 | 68, 69, 33 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
((#‘𝐴) +
(#‘𝐵)) =
((#‘𝐵) +
(#‘𝐴))) |
71 | 70 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(0..^((#‘𝐴) +
(#‘𝐵))) =
(0..^((#‘𝐵) +
(#‘𝐴)))) |
72 | 71 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↔ (𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐵) + (#‘𝐴))))) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ((𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↔ (𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐵) + (#‘𝐴))))) |
74 | 67, 73 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐴) + (#‘𝐵)))) |
75 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 + (#‘𝐴)) → (𝑥 ∈ (0..^(#‘𝐴)) ↔ (𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)))) |
76 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 + (#‘𝐴)) → (𝐴‘𝑥) = (𝐴‘(𝑦 + (#‘𝐴)))) |
77 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑦 + (#‘𝐴)) → (𝑥 − (#‘𝐴)) = ((𝑦 + (#‘𝐴)) − (#‘𝐴))) |
78 | 77 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 + (#‘𝐴)) → (𝐵‘(𝑥 − (#‘𝐴))) = (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) |
79 | 75, 76, 78 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 + (#‘𝐴)) → if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) = if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴))))) |
80 | 79 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 + (#‘𝐴)) → (if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 ↔ if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) ∈ 𝑆)) |
81 | 80 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 + (#‘𝐴)) ∈ (0..^((#‘𝐴) + (#‘𝐵))) → (∀𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) ∈ 𝑆)) |
82 | 74, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (∀𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) ∈ 𝑆)) |
83 | 18 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ Word V →
(#‘𝐴) ∈
ℝ) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘𝐴) ∈
ℝ) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (#‘𝐴) ∈
ℝ) |
86 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (0..^(#‘𝐵)) → 𝑦 ∈ ℤ) |
87 | 86 | zred 11358 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ (0..^(#‘𝐵)) → 𝑦 ∈ ℝ) |
88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (0..^(#‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → 𝑦 ∈ ℝ) |
89 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (0..^(#‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → (#‘𝐴) ∈
ℝ) |
90 | 88, 89 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ∈ (0..^(#‘𝐵)) ∧ (𝐴 ∈ Word V ∧ 𝐵 ∈ Word V)) → (𝑦 + (#‘𝐴)) ∈ ℝ) |
91 | 90 | ancoms 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (𝑦 + (#‘𝐴)) ∈ ℝ) |
92 | | elfzole1 12347 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (0..^(#‘𝐵)) → 0 ≤ 𝑦) |
93 | 92 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → 0 ≤ 𝑦) |
94 | | addge02 10418 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝐴) ∈
ℝ ∧ 𝑦 ∈
ℝ) → (0 ≤ 𝑦
↔ (#‘𝐴) ≤
(𝑦 + (#‘𝐴)))) |
95 | 84, 87, 94 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (0 ≤ 𝑦 ↔ (#‘𝐴) ≤ (𝑦 + (#‘𝐴)))) |
96 | 93, 95 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (#‘𝐴) ≤ (𝑦 + (#‘𝐴))) |
97 | 85, 91, 96 | lensymd 10067 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ¬ (𝑦 + (#‘𝐴)) < (#‘𝐴)) |
98 | 97 | intn3an3d 1436 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ¬ ((𝑦 + (#‘𝐴)) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝑦 + (#‘𝐴)) < (#‘𝐴))) |
99 | | elfzo0 12376 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)) ↔ ((𝑦 + (#‘𝐴)) ∈ ℕ0 ∧
(#‘𝐴) ∈ ℕ
∧ (𝑦 + (#‘𝐴)) < (#‘𝐴))) |
100 | 98, 99 | sylnibr 318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ¬ (𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴))) |
101 | 100 | iffalsed 4047 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) = (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) |
102 | 101 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) ∈ 𝑆 ↔ (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴))) ∈ 𝑆)) |
103 | 86 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (0..^(#‘𝐵)) → 𝑦 ∈ ℂ) |
104 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(#‘𝐴) ∈
ℂ) |
105 | | pncan 10166 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℂ ∧
(#‘𝐴) ∈ ℂ)
→ ((𝑦 + (#‘𝐴)) − (#‘𝐴)) = 𝑦) |
106 | 103, 104,
105 | syl2anr 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ((𝑦 + (#‘𝐴)) − (#‘𝐴)) = 𝑦) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴))) = (𝐵‘𝑦)) |
108 | 107 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ((𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴))) ∈ 𝑆 ↔ (𝐵‘𝑦) ∈ 𝑆)) |
109 | 108 | biimpd 218 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → ((𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆)) |
110 | 102, 109 | sylbid 229 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (if((𝑦 + (#‘𝐴)) ∈ (0..^(#‘𝐴)), (𝐴‘(𝑦 + (#‘𝐴))), (𝐵‘((𝑦 + (#‘𝐴)) − (#‘𝐴)))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆)) |
111 | 82, 110 | syld 46 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (∀𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → (𝐵‘𝑦) ∈ 𝑆)) |
112 | 111 | impancom 455 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → (𝑦 ∈ (0..^(#‘𝐵)) → (𝐵‘𝑦) ∈ 𝑆)) |
113 | 112 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) ∧ 𝑦 ∈ (0..^(#‘𝐵))) → (𝐵‘𝑦) ∈ 𝑆) |
114 | 113 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → ∀𝑦 ∈ (0..^(#‘𝐵))(𝐵‘𝑦) ∈ 𝑆) |
115 | | iswrdsymb 13177 |
. . . . . . . . 9
⊢ ((𝐵 ∈ Word V ∧
∀𝑦 ∈
(0..^(#‘𝐵))(𝐵‘𝑦) ∈ 𝑆) → 𝐵 ∈ Word 𝑆) |
116 | 62, 114, 115 | syl2an2r 872 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → 𝐵 ∈ Word 𝑆) |
117 | 61, 116 | jca 553 |
. . . . . . 7
⊢ (((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) ∧
∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆) → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)) |
118 | 117 | ex 449 |
. . . . . 6
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) →
(∀𝑥 ∈
(0..^((#‘𝐴) +
(#‘𝐵)))if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))) ∈ 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |
119 | 29, 118 | syl5bir 232 |
. . . . 5
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))):(0..^((#‘𝐴) + (#‘𝐵)))⟶𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |
120 | 27, 119 | sylbid 229 |
. . . 4
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))):(0..^(#‘(𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴)))))))⟶𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |
121 | 3, 120 | syl5 33 |
. . 3
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝑥 ∈ (0..^((#‘𝐴) + (#‘𝐵))) ↦ if(𝑥 ∈ (0..^(#‘𝐴)), (𝐴‘𝑥), (𝐵‘(𝑥 − (#‘𝐴))))) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |
122 | 2, 121 | sylbid 229 |
. 2
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 → (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |
123 | | ccatcl 13212 |
. 2
⊢ ((𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆) → (𝐴 ++ 𝐵) ∈ Word 𝑆) |
124 | 122, 123 | impbid1 214 |
1
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆))) |