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∈WordB∧T∈WordB→ran⁡S++T=ran⁡S∪ran⁡T

Proof

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