Metamath Proof Explorer

Theorem ccatrn

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

Ref Expression
Assertion ccatrn ⊢ S ∈ Word B ∧ T ∈ Word B → ran ⁡ S ++ T = ran ⁡ S ∪ ran ⁡ T

Proof

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