Step | Hyp | Ref
| Expression |
1 | | ccatvalfn 13365 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) Fn (0..^((#‘𝑆) + (#‘𝑇)))) |
2 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (#‘𝑆) ∈
ℕ0) |
3 | 2 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
ℕ0) |
4 | | nn0uz 11722 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
5 | 3, 4 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘0)) |
6 | 3 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ ℤ) |
7 | | uzid 11702 |
. . . . . . . . . . . 12
⊢
((#‘𝑆) ∈
ℤ → (#‘𝑆)
∈ (ℤ≥‘(#‘𝑆))) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘(#‘𝑆))) |
9 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ Word 𝐵 → (#‘𝑇) ∈
ℕ0) |
10 | 9 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑇) ∈
ℕ0) |
11 | | uzaddcl 11744 |
. . . . . . . . . . 11
⊢
(((#‘𝑆) ∈
(ℤ≥‘(#‘𝑆)) ∧ (#‘𝑇) ∈ ℕ0) →
((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
12 | 8, 10, 11 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
13 | | elfzuzb 12336 |
. . . . . . . . . 10
⊢
((#‘𝑆) ∈
(0...((#‘𝑆) +
(#‘𝑇))) ↔
((#‘𝑆) ∈
(ℤ≥‘0) ∧ ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆)))) |
14 | 5, 12, 13 | sylanbrc 698 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑆) ∈ (0...((#‘𝑆) + (#‘𝑇)))) |
15 | | fzosplit 12501 |
. . . . . . . . 9
⊢
((#‘𝑆) ∈
(0...((#‘𝑆) +
(#‘𝑇))) →
(0..^((#‘𝑆) +
(#‘𝑇))) =
((0..^(#‘𝑆)) ∪
((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^((#‘𝑆) + (#‘𝑇))) = ((0..^(#‘𝑆)) ∪ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) |
17 | 16 | eleq2d 2687 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↔ 𝑥 ∈ ((0..^(#‘𝑆)) ∪ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))))) |
18 | | elun 3753 |
. . . . . . 7
⊢ (𝑥 ∈ ((0..^(#‘𝑆)) ∪ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) ↔ (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) |
19 | 17, 18 | syl6bb 276 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↔ (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))))) |
20 | | ccatval1 13361 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) |
21 | 20 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) |
22 | | ssun1 3776 |
. . . . . . . . . 10
⊢ ran 𝑆 ⊆ (ran 𝑆 ∪ ran 𝑇) |
23 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆 ∈ Word 𝐵) |
24 | | wrdf 13310 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → 𝑆:(0..^(#‘𝑆))⟶𝐵) |
25 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝑆:(0..^(#‘𝑆))⟶𝐵 → 𝑆 Fn (0..^(#‘𝑆))) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆 Fn (0..^(#‘𝑆))) |
27 | | fnfvelrn 6356 |
. . . . . . . . . . 11
⊢ ((𝑆 Fn (0..^(#‘𝑆)) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆‘𝑥) ∈ ran 𝑆) |
28 | 26, 27 | sylan 488 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆‘𝑥) ∈ ran 𝑆) |
29 | 22, 28 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
30 | 21, 29 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
31 | | ccatval2 13362 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (#‘𝑆)))) |
32 | 31 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (#‘𝑆)))) |
33 | | ssun2 3777 |
. . . . . . . . . 10
⊢ ran 𝑇 ⊆ (ran 𝑆 ∪ ran 𝑇) |
34 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇 ∈ Word 𝐵) |
35 | | wrdf 13310 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Word 𝐵 → 𝑇:(0..^(#‘𝑇))⟶𝐵) |
36 | | ffn 6045 |
. . . . . . . . . . . . 13
⊢ (𝑇:(0..^(#‘𝑇))⟶𝐵 → 𝑇 Fn (0..^(#‘𝑇))) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇 Fn (0..^(#‘𝑇))) |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑇 Fn (0..^(#‘𝑇))) |
39 | | elfzouz 12474 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) → 𝑥 ∈
(ℤ≥‘(#‘𝑆))) |
40 | 39 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 ∈
(ℤ≥‘(#‘𝑆))) |
41 | | uznn0sub 11719 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
(ℤ≥‘(#‘𝑆)) → (𝑥 − (#‘𝑆)) ∈
ℕ0) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 − (#‘𝑆)) ∈
ℕ0) |
43 | 42, 4 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 − (#‘𝑆)) ∈
(ℤ≥‘0)) |
44 | 10 | nn0zd 11480 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘𝑇) ∈ ℤ) |
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (#‘𝑇) ∈ ℤ) |
46 | | elfzolt2 12479 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) → 𝑥 < ((#‘𝑆) + (#‘𝑇))) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 < ((#‘𝑆) + (#‘𝑇))) |
48 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) → 𝑥 ∈ ℤ) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 ∈ ℤ) |
50 | 49 | zred 11482 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 ∈ ℝ) |
51 | 6 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (#‘𝑆) ∈ ℤ) |
52 | 51 | zred 11482 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (#‘𝑆) ∈ ℝ) |
53 | 45 | zred 11482 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (#‘𝑇) ∈ ℝ) |
54 | 50, 52, 53 | ltsubadd2d 10625 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑥 − (#‘𝑆)) < (#‘𝑇) ↔ 𝑥 < ((#‘𝑆) + (#‘𝑇)))) |
55 | 47, 54 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 − (#‘𝑆)) < (#‘𝑇)) |
56 | | elfzo2 12473 |
. . . . . . . . . . . 12
⊢ ((𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇)) ↔ ((𝑥 − (#‘𝑆)) ∈ (ℤ≥‘0)
∧ (#‘𝑇) ∈
ℤ ∧ (𝑥 −
(#‘𝑆)) <
(#‘𝑇))) |
57 | 43, 45, 55, 56 | syl3anbrc 1246 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) |
58 | | fnfvelrn 6356 |
. . . . . . . . . . 11
⊢ ((𝑇 Fn (0..^(#‘𝑇)) ∧ (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) → (𝑇‘(𝑥 − (#‘𝑆))) ∈ ran 𝑇) |
59 | 38, 57, 58 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑇‘(𝑥 − (#‘𝑆))) ∈ ran 𝑇) |
60 | 33, 59 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑇‘(𝑥 − (#‘𝑆))) ∈ (ran 𝑆 ∪ ran 𝑇)) |
61 | 32, 60 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
62 | 30, 61 | jaodan 826 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
63 | 62 | ex 450 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) |
64 | 19, 63 | sylbid 230 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) |
65 | 64 | ralrimiv 2965 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
66 | | ffnfv 6388 |
. . . 4
⊢ ((𝑆 ++ 𝑇):(0..^((#‘𝑆) + (#‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇) ↔ ((𝑆 ++ 𝑇) Fn (0..^((#‘𝑆) + (#‘𝑇))) ∧ ∀𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) |
67 | 1, 65, 66 | sylanbrc 698 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇):(0..^((#‘𝑆) + (#‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇)) |
68 | | frn 6053 |
. . 3
⊢ ((𝑆 ++ 𝑇):(0..^((#‘𝑆) + (#‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇) → ran (𝑆 ++ 𝑇) ⊆ (ran 𝑆 ∪ ran 𝑇)) |
69 | 67, 68 | syl 17 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) ⊆ (ran 𝑆 ∪ ran 𝑇)) |
70 | 1 | adantr 481 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆 ++ 𝑇) Fn (0..^((#‘𝑆) + (#‘𝑇)))) |
71 | | fzoss2 12496 |
. . . . . . . . . 10
⊢
(((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆)) → (0..^(#‘𝑆)) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
72 | 12, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(#‘𝑆)) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
73 | 72 | sselda 3603 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) |
74 | | fnfvelrn 6356 |
. . . . . . . 8
⊢ (((𝑆 ++ 𝑇) Fn (0..^((#‘𝑆) + (#‘𝑇))) ∧ 𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
75 | 70, 73, 74 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
76 | 21, 75 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
77 | 76 | ralrimiva 2966 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^(#‘𝑆))(𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
78 | | ffnfv 6388 |
. . . . 5
⊢ (𝑆:(0..^(#‘𝑆))⟶ran (𝑆 ++ 𝑇) ↔ (𝑆 Fn (0..^(#‘𝑆)) ∧ ∀𝑥 ∈ (0..^(#‘𝑆))(𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇))) |
79 | 26, 77, 78 | sylanbrc 698 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆:(0..^(#‘𝑆))⟶ran (𝑆 ++ 𝑇)) |
80 | | frn 6053 |
. . . 4
⊢ (𝑆:(0..^(#‘𝑆))⟶ran (𝑆 ++ 𝑇) → ran 𝑆 ⊆ ran (𝑆 ++ 𝑇)) |
81 | 79, 80 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran 𝑆 ⊆ ran (𝑆 ++ 𝑇)) |
82 | | ccatval3 13363 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (#‘𝑆))) = (𝑇‘𝑥)) |
83 | 82 | 3expa 1265 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (#‘𝑆))) = (𝑇‘𝑥)) |
84 | 1 | adantr 481 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑆 ++ 𝑇) Fn (0..^((#‘𝑆) + (#‘𝑇)))) |
85 | | elfzouz 12474 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (0..^(#‘𝑇)) → 𝑥 ∈
(ℤ≥‘0)) |
86 | 85 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈
(ℤ≥‘0)) |
87 | 86, 4 | syl6eleqr 2712 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ ℕ0) |
88 | 3 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (#‘𝑆) ∈
ℕ0) |
89 | 87, 88 | nn0addcld 11355 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑥 + (#‘𝑆)) ∈
ℕ0) |
90 | 89, 4 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑥 + (#‘𝑆)) ∈
(ℤ≥‘0)) |
91 | 3, 10 | nn0addcld 11355 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
ℕ0) |
92 | 91 | nn0zd 11480 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈ ℤ) |
93 | 92 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((#‘𝑆) + (#‘𝑇)) ∈ ℤ) |
94 | 87 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ ℂ) |
95 | 88 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (#‘𝑆) ∈ ℂ) |
96 | 94, 95 | addcomd 10238 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑥 + (#‘𝑆)) = ((#‘𝑆) + 𝑥)) |
97 | 87 | nn0red 11352 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 ∈ ℝ) |
98 | 10 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (#‘𝑇) ∈
ℕ0) |
99 | 98 | nn0red 11352 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (#‘𝑇) ∈ ℝ) |
100 | 88 | nn0red 11352 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (#‘𝑆) ∈ ℝ) |
101 | | elfzolt2 12479 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (0..^(#‘𝑇)) → 𝑥 < (#‘𝑇)) |
102 | 101 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → 𝑥 < (#‘𝑇)) |
103 | 97, 99, 100, 102 | ltadd2dd 10196 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((#‘𝑆) + 𝑥) < ((#‘𝑆) + (#‘𝑇))) |
104 | 96, 103 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑥 + (#‘𝑆)) < ((#‘𝑆) + (#‘𝑇))) |
105 | | elfzo2 12473 |
. . . . . . . . 9
⊢ ((𝑥 + (#‘𝑆)) ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↔ ((𝑥 + (#‘𝑆)) ∈ (ℤ≥‘0)
∧ ((#‘𝑆) +
(#‘𝑇)) ∈ ℤ
∧ (𝑥 + (#‘𝑆)) < ((#‘𝑆) + (#‘𝑇)))) |
106 | 90, 93, 104, 105 | syl3anbrc 1246 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑥 + (#‘𝑆)) ∈ (0..^((#‘𝑆) + (#‘𝑇)))) |
107 | | fnfvelrn 6356 |
. . . . . . . 8
⊢ (((𝑆 ++ 𝑇) Fn (0..^((#‘𝑆) + (#‘𝑇))) ∧ (𝑥 + (#‘𝑆)) ∈ (0..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘(𝑥 + (#‘𝑆))) ∈ ran (𝑆 ++ 𝑇)) |
108 | 84, 106, 107 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (#‘𝑆))) ∈ ran (𝑆 ++ 𝑇)) |
109 | 83, 108 | eqeltrrd 2702 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑇))) → (𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
110 | 109 | ralrimiva 2966 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^(#‘𝑇))(𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
111 | | ffnfv 6388 |
. . . . 5
⊢ (𝑇:(0..^(#‘𝑇))⟶ran (𝑆 ++ 𝑇) ↔ (𝑇 Fn (0..^(#‘𝑇)) ∧ ∀𝑥 ∈ (0..^(#‘𝑇))(𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇))) |
112 | 37, 110, 111 | sylanbrc 698 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇:(0..^(#‘𝑇))⟶ran (𝑆 ++ 𝑇)) |
113 | | frn 6053 |
. . . 4
⊢ (𝑇:(0..^(#‘𝑇))⟶ran (𝑆 ++ 𝑇) → ran 𝑇 ⊆ ran (𝑆 ++ 𝑇)) |
114 | 112, 113 | syl 17 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran 𝑇 ⊆ ran (𝑆 ++ 𝑇)) |
115 | 81, 114 | unssd 3789 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (ran 𝑆 ∪ ran 𝑇) ⊆ ran (𝑆 ++ 𝑇)) |
116 | 69, 115 | eqssd 3620 |
1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) |