Metamath Proof Explorer

Theorem ccatrn

Description: The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion ccatrn ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ran ( 𝑆 ++ 𝑇 ) = ( ran 𝑆 ∪ ran 𝑇 ) )

Proof

Step Hyp Ref Expression
1 ccatvalfn ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
2 lencl ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
3 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4 2 3 eleqtrdi ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
5 4 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
6 2 nn0zd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℤ )
7 6 uzidd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
8 lencl ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
9 uzaddcl ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
10 7 8 9 syl2an ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
11 elfzuzb ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↔ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) ) )
12 5 10 11 sylanbrc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
13 fzosplit ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
14 12 13 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
15 14 eleq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↔ 𝑥 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ) )
16 elun ⊢ ( 𝑥 ∈ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
17 15 16 bitrdi ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ) )
18 ccatval1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
19 18 3expa ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
20 ssun1 ⊢ ran 𝑆 ⊆ ( ran 𝑆 ∪ ran 𝑇 )
21 wrdfn ⊢ ( 𝑆 ∈ Word 𝐵 → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
22 21 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
23 fnfvelrn ⊢ ( ( 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ran 𝑆 )
24 22 23 sylan ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ran 𝑆 )
25 20 24 sseldi ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) )
26 19 25 eqeltrd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) )
27 ccatval2 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
28 27 3expa ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
29 ssun2 ⊢ ran 𝑇 ⊆ ( ran 𝑆 ∪ ran 𝑇 )
30 wrdfn ⊢ ( 𝑇 ∈ Word 𝐵 → 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
31 30 adantl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
32 elfzouz ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
33 uznn0sub ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ℕ0 )
34 32 33 syl ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ℕ0 )
35 34 3 eleqtrdi ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( ℤ≥ ‘ 0 ) )
36 35 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( ℤ≥ ‘ 0 ) )
37 8 nn0zd ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℤ )
38 37 ad2antlr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ♯ ‘ 𝑇 ) ∈ ℤ )
39 elfzolt2 ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → 𝑥 < ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
40 39 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 < ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
41 elfzoelz ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ℤ )
42 41 zred ⊢ ( 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ℝ )
43 42 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → 𝑥 ∈ ℝ )
44 2 nn0red ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℝ )
45 44 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ℝ )
46 8 nn0red ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℝ )
47 46 ad2antlr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ♯ ‘ 𝑇 ) ∈ ℝ )
48 43 45 47 ltsubadd2d ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) < ( ♯ ‘ 𝑇 ) ↔ 𝑥 < ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
49 40 48 mpbird ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) < ( ♯ ‘ 𝑇 ) )
50 elfzo2 ⊢ ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ↔ ( ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℤ ∧ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) < ( ♯ ‘ 𝑇 ) ) )
51 36 38 49 50 syl3anbrc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
52 fnfvelrn ⊢ ( ( 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ∈ ran 𝑇 )
53 31 51 52 syl2an2r ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ∈ ran 𝑇 )
54 29 53 sseldi ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) )
55 28 54 eqeltrd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) )
56 26 55 jaodan ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) )
57 56 ex ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∨ 𝑥 ∈ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) ) )
58 17 57 sylbid ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) ) )
59 58 ralrimiv ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) )
60 ffnfv ⊢ ( ( 𝑆 ++ 𝑇 ) : ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⟶ ( ran 𝑆 ∪ ran 𝑇 ) ↔ ( ( 𝑆 ++ 𝑇 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ( ran 𝑆 ∪ ran 𝑇 ) ) )
61 1 59 60 sylanbrc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) : ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ⟶ ( ran 𝑆 ∪ ran 𝑇 ) )
62 61 frnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ran ( 𝑆 ++ 𝑇 ) ⊆ ( ran 𝑆 ∪ ran 𝑇 ) )
63 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
64 10 63 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
65 64 sselda ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
66 fnfvelrn ⊢ ( ( ( 𝑆 ++ 𝑇 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) )
67 1 65 66 syl2an2r ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) )
68 19 67 eqeltrrd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) )
69 68 ralrimiva ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ( 𝑆 ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) )
70 ffnfv ⊢ ( 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ ran ( 𝑆 ++ 𝑇 ) ↔ ( 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ( 𝑆 ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) ) )
71 22 69 70 sylanbrc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → 𝑆 : ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⟶ ran ( 𝑆 ++ 𝑇 ) )
72 71 frnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ran 𝑆 ⊆ ran ( 𝑆 ++ 𝑇 ) )
73 ccatval3 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ 𝑥 ) )
74 73 3expa ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ) = ( 𝑇 ‘ 𝑥 ) )
75 elfzouz ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 0 ) )
76 2 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
77 uzaddcl ⊢ ( ( 𝑥 ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝑆 ) ∈ ℕ0 ) → ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ∈ ( ℤ≥ ‘ 0 ) )
78 75 76 77 syl2anr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ∈ ( ℤ≥ ‘ 0 ) )
79 nn0addcl ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℕ0 )
80 2 8 79 syl2an ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℕ0 )
81 80 nn0zd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℤ )
82 81 adantr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℤ )
83 elfzonn0 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) → 𝑥 ∈ ℕ0 )
84 83 nn0cnd ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) → 𝑥 ∈ ℂ )
85 2 nn0cnd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℂ )
86 85 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ℂ )
87 addcom ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ♯ ‘ 𝑆 ) ∈ ℂ ) → ( 𝑥 + ( ♯ ‘ 𝑆 ) ) = ( ( ♯ ‘ 𝑆 ) + 𝑥 ) )
88 84 86 87 syl2anr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 + ( ♯ ‘ 𝑆 ) ) = ( ( ♯ ‘ 𝑆 ) + 𝑥 ) )
89 83 nn0red ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) → 𝑥 ∈ ℝ )
90 89 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 ∈ ℝ )
91 46 ad2antlr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ♯ ‘ 𝑇 ) ∈ ℝ )
92 44 ad2antrr ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ♯ ‘ 𝑆 ) ∈ ℝ )
93 elfzolt2 ⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) → 𝑥 < ( ♯ ‘ 𝑇 ) )
94 93 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → 𝑥 < ( ♯ ‘ 𝑇 ) )
95 90 91 92 94 ltadd2dd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( ♯ ‘ 𝑆 ) + 𝑥 ) < ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
96 88 95 eqbrtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 + ( ♯ ‘ 𝑆 ) ) < ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
97 elfzo2 ⊢ ( ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↔ ( ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℤ ∧ ( 𝑥 + ( ♯ ‘ 𝑆 ) ) < ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
98 78 82 96 97 syl3anbrc ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
99 fnfvelrn ⊢ ( ( ( 𝑆 ++ 𝑇 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∧ ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ) ∈ ran ( 𝑆 ++ 𝑇 ) )
100 1 98 99 syl2an2r ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ ( 𝑥 + ( ♯ ‘ 𝑆 ) ) ) ∈ ran ( 𝑆 ++ 𝑇 ) )
101 74 100 eqeltrrd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) )
102 101 ralrimiva ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ( 𝑇 ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) )
103 ffnfv ⊢ ( 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ ran ( 𝑆 ++ 𝑇 ) ↔ ( 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ( 𝑇 ‘ 𝑥 ) ∈ ran ( 𝑆 ++ 𝑇 ) ) )
104 31 102 103 sylanbrc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ ran ( 𝑆 ++ 𝑇 ) )
105 104 frnd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ran 𝑇 ⊆ ran ( 𝑆 ++ 𝑇 ) )
106 72 105 unssd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ran 𝑆 ∪ ran 𝑇 ) ⊆ ran ( 𝑆 ++ 𝑇 ) )
107 62 106 eqssd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ran ( 𝑆 ++ 𝑇 ) = ( ran 𝑆 ∪ ran 𝑇 ) )