Step | Hyp | Ref
| Expression |
1 | | ccatvalfn 14286 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇)))) |
2 | | lencl 14236 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
ℕ0) |
3 | | nn0uz 12620 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
4 | 2, 3 | eleqtrdi 2849 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
(ℤ≥‘0)) |
5 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
(ℤ≥‘0)) |
6 | 2 | nn0zd 12424 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℤ) |
7 | 6 | uzidd 12598 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈
(ℤ≥‘(♯‘𝑆))) |
8 | | lencl 14236 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈
ℕ0) |
9 | | uzaddcl 12644 |
. . . . . . . . . . 11
⊢
(((♯‘𝑆)
∈ (ℤ≥‘(♯‘𝑆)) ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) |
10 | 7, 8, 9 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆))) |
11 | | elfzuzb 13250 |
. . . . . . . . . 10
⊢
((♯‘𝑆)
∈ (0...((♯‘𝑆) + (♯‘𝑇))) ↔ ((♯‘𝑆) ∈ (ℤ≥‘0)
∧ ((♯‘𝑆) +
(♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆)))) |
12 | 5, 10, 11 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ (0...((♯‘𝑆) + (♯‘𝑇)))) |
13 | | fzosplit 13420 |
. . . . . . . . 9
⊢
((♯‘𝑆)
∈ (0...((♯‘𝑆) + (♯‘𝑇))) → (0..^((♯‘𝑆) + (♯‘𝑇))) = ((0..^(♯‘𝑆)) ∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^((♯‘𝑆) + (♯‘𝑇))) = ((0..^(♯‘𝑆)) ∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) |
15 | 14 | eleq2d 2824 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↔ 𝑥 ∈ ((0..^(♯‘𝑆)) ∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))) |
16 | | elun 4083 |
. . . . . . 7
⊢ (𝑥 ∈
((0..^(♯‘𝑆))
∪ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) ↔ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) |
17 | 15, 16 | bitrdi 287 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↔ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))))) |
18 | | ccatval1 14281 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) |
19 | 18 | 3expa 1117 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) |
20 | | ssun1 4106 |
. . . . . . . . . 10
⊢ ran 𝑆 ⊆ (ran 𝑆 ∪ ran 𝑇) |
21 | | wrdfn 14231 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → 𝑆 Fn (0..^(♯‘𝑆))) |
22 | 21 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆 Fn (0..^(♯‘𝑆))) |
23 | | fnfvelrn 6958 |
. . . . . . . . . . 11
⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ ran 𝑆) |
24 | 22, 23 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ ran 𝑆) |
25 | 20, 24 | sselid 3919 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
26 | 19, 25 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
27 | | ccatval2 14283 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (♯‘𝑆)))) |
28 | 27 | 3expa 1117 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (♯‘𝑆)))) |
29 | | ssun2 4107 |
. . . . . . . . . 10
⊢ ran 𝑇 ⊆ (ran 𝑆 ∪ ran 𝑇) |
30 | | wrdfn 14231 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ Word 𝐵 → 𝑇 Fn (0..^(♯‘𝑇))) |
31 | 30 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇 Fn (0..^(♯‘𝑇))) |
32 | | elfzouz 13391 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 ∈
(ℤ≥‘(♯‘𝑆))) |
33 | | uznn0sub 12617 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
(ℤ≥‘(♯‘𝑆)) → (𝑥 − (♯‘𝑆)) ∈
ℕ0) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → (𝑥 − (♯‘𝑆)) ∈
ℕ0) |
35 | 34, 3 | eleqtrdi 2849 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → (𝑥 − (♯‘𝑆)) ∈
(ℤ≥‘0)) |
36 | 35 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) ∈
(ℤ≥‘0)) |
37 | 8 | nn0zd 12424 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈ ℤ) |
38 | 37 | ad2antlr 724 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (♯‘𝑇) ∈ ℤ) |
39 | | elfzolt2 13396 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 < ((♯‘𝑆) + (♯‘𝑇))) |
40 | 39 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 < ((♯‘𝑆) + (♯‘𝑇))) |
41 | | elfzoelz 13387 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 ∈ ℤ) |
42 | 41 | zred 12426 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))) → 𝑥 ∈ ℝ) |
43 | 42 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → 𝑥 ∈ ℝ) |
44 | 2 | nn0red 12294 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℝ) |
45 | 44 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (♯‘𝑆) ∈ ℝ) |
46 | 8 | nn0red 12294 |
. . . . . . . . . . . . . . 15
⊢ (𝑇 ∈ Word 𝐵 → (♯‘𝑇) ∈ ℝ) |
47 | 46 | ad2antlr 724 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (♯‘𝑇) ∈ ℝ) |
48 | 43, 45, 47 | ltsubadd2d 11573 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑥 − (♯‘𝑆)) < (♯‘𝑇) ↔ 𝑥 < ((♯‘𝑆) + (♯‘𝑇)))) |
49 | 40, 48 | mpbird 256 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) < (♯‘𝑇)) |
50 | | elfzo2 13390 |
. . . . . . . . . . . 12
⊢ ((𝑥 − (♯‘𝑆)) ∈
(0..^(♯‘𝑇))
↔ ((𝑥 −
(♯‘𝑆)) ∈
(ℤ≥‘0) ∧ (♯‘𝑇) ∈ ℤ ∧ (𝑥 − (♯‘𝑆)) < (♯‘𝑇))) |
51 | 36, 38, 49, 50 | syl3anbrc 1342 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) |
52 | | fnfvelrn 6958 |
. . . . . . . . . . 11
⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (𝑥 − (♯‘𝑆)) ∈ (0..^(♯‘𝑇))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ ran 𝑇) |
53 | 31, 51, 52 | syl2an2r 682 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ ran 𝑇) |
54 | 29, 53 | sselid 3919 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → (𝑇‘(𝑥 − (♯‘𝑆))) ∈ (ran 𝑆 ∪ ran 𝑇)) |
55 | 28, 54 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
56 | 26, 55 | jaodan 955 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ (𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇))))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
57 | 56 | ex 413 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑥 ∈ (0..^(♯‘𝑆)) ∨ 𝑥 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) |
58 | 17, 57 | sylbid 239 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) |
59 | 58 | ralrimiv 3102 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇)) |
60 | | ffnfv 6992 |
. . . 4
⊢ ((𝑆 ++ 𝑇):(0..^((♯‘𝑆) + (♯‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇) ↔ ((𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ ∀𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))((𝑆 ++ 𝑇)‘𝑥) ∈ (ran 𝑆 ∪ ran 𝑇))) |
61 | 1, 59, 60 | sylanbrc 583 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇):(0..^((♯‘𝑆) + (♯‘𝑇)))⟶(ran 𝑆 ∪ ran 𝑇)) |
62 | 61 | frnd 6608 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) ⊆ (ran 𝑆 ∪ ran 𝑇)) |
63 | | fzoss2 13415 |
. . . . . . . . . 10
⊢
(((♯‘𝑆)
+ (♯‘𝑇)) ∈
(ℤ≥‘(♯‘𝑆)) → (0..^(♯‘𝑆)) ⊆
(0..^((♯‘𝑆) +
(♯‘𝑇)))) |
64 | 10, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (0..^(♯‘𝑆)) ⊆
(0..^((♯‘𝑆) +
(♯‘𝑇)))) |
65 | 64 | sselda 3921 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) |
66 | | fnfvelrn 6958 |
. . . . . . . 8
⊢ (((𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ 𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
67 | 1, 65, 66 | syl2an2r 682 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
68 | 19, 67 | eqeltrrd 2840 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑆))) → (𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
69 | 68 | ralrimiva 3103 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^(♯‘𝑆))(𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
70 | | ffnfv 6992 |
. . . . 5
⊢ (𝑆:(0..^(♯‘𝑆))⟶ran (𝑆 ++ 𝑇) ↔ (𝑆 Fn (0..^(♯‘𝑆)) ∧ ∀𝑥 ∈ (0..^(♯‘𝑆))(𝑆‘𝑥) ∈ ran (𝑆 ++ 𝑇))) |
71 | 22, 69, 70 | sylanbrc 583 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑆:(0..^(♯‘𝑆))⟶ran (𝑆 ++ 𝑇)) |
72 | 71 | frnd 6608 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran 𝑆 ⊆ ran (𝑆 ++ 𝑇)) |
73 | | ccatval3 14284 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) = (𝑇‘𝑥)) |
74 | 73 | 3expa 1117 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) = (𝑇‘𝑥)) |
75 | | elfzouz 13391 |
. . . . . . . . . 10
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
(ℤ≥‘0)) |
76 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈
ℕ0) |
77 | | uzaddcl 12644 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘0) ∧ (♯‘𝑆) ∈ ℕ0) → (𝑥 + (♯‘𝑆)) ∈
(ℤ≥‘0)) |
78 | 75, 76, 77 | syl2anr 597 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) ∈
(ℤ≥‘0)) |
79 | | nn0addcl 12268 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑆)
∈ ℕ0 ∧ (♯‘𝑇) ∈ ℕ0) →
((♯‘𝑆) +
(♯‘𝑇)) ∈
ℕ0) |
80 | 2, 8, 79 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈
ℕ0) |
81 | 80 | nn0zd 12424 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ) |
82 | 81 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ) |
83 | | elfzonn0 13432 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℕ0) |
84 | 83 | nn0cnd 12295 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℂ) |
85 | 2 | nn0cnd 12295 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Word 𝐵 → (♯‘𝑆) ∈ ℂ) |
86 | 85 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘𝑆) ∈ ℂ) |
87 | | addcom 11161 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧
(♯‘𝑆) ∈
ℂ) → (𝑥 +
(♯‘𝑆)) =
((♯‘𝑆) + 𝑥)) |
88 | 84, 86, 87 | syl2anr 597 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) = ((♯‘𝑆) + 𝑥)) |
89 | 83 | nn0red 12294 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 ∈
ℝ) |
90 | 89 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℝ) |
91 | 46 | ad2antlr 724 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑇) ∈ ℝ) |
92 | 44 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑆) ∈ ℝ) |
93 | | elfzolt2 13396 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(0..^(♯‘𝑇))
→ 𝑥 <
(♯‘𝑇)) |
94 | 93 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 < (♯‘𝑇)) |
95 | 90, 91, 92, 94 | ltadd2dd 11134 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑆) + 𝑥) < ((♯‘𝑆) + (♯‘𝑇))) |
96 | 88, 95 | eqbrtrd 5096 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) < ((♯‘𝑆) + (♯‘𝑇))) |
97 | | elfzo2 13390 |
. . . . . . . . 9
⊢ ((𝑥 + (♯‘𝑆)) ∈
(0..^((♯‘𝑆) +
(♯‘𝑇))) ↔
((𝑥 + (♯‘𝑆)) ∈
(ℤ≥‘0) ∧ ((♯‘𝑆) + (♯‘𝑇)) ∈ ℤ ∧ (𝑥 + (♯‘𝑆)) < ((♯‘𝑆) + (♯‘𝑇)))) |
98 | 78, 82, 96, 97 | syl3anbrc 1342 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑥 + (♯‘𝑆)) ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) |
99 | | fnfvelrn 6958 |
. . . . . . . 8
⊢ (((𝑆 ++ 𝑇) Fn (0..^((♯‘𝑆) + (♯‘𝑇))) ∧ (𝑥 + (♯‘𝑆)) ∈ (0..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) ∈ ran (𝑆 ++ 𝑇)) |
100 | 1, 98, 99 | syl2an2r 682 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝑥 + (♯‘𝑆))) ∈ ran (𝑆 ++ 𝑇)) |
101 | 74, 100 | eqeltrrd 2840 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
102 | 101 | ralrimiva 3103 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ∀𝑥 ∈ (0..^(♯‘𝑇))(𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇)) |
103 | | ffnfv 6992 |
. . . . 5
⊢ (𝑇:(0..^(♯‘𝑇))⟶ran (𝑆 ++ 𝑇) ↔ (𝑇 Fn (0..^(♯‘𝑇)) ∧ ∀𝑥 ∈ (0..^(♯‘𝑇))(𝑇‘𝑥) ∈ ran (𝑆 ++ 𝑇))) |
104 | 31, 102, 103 | sylanbrc 583 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → 𝑇:(0..^(♯‘𝑇))⟶ran (𝑆 ++ 𝑇)) |
105 | 104 | frnd 6608 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran 𝑇 ⊆ ran (𝑆 ++ 𝑇)) |
106 | 72, 105 | unssd 4120 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (ran 𝑆 ∪ ran 𝑇) ⊆ ran (𝑆 ++ 𝑇)) |
107 | 62, 106 | eqssd 3938 |
1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) |