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 e. Word B /\ T e. Word B ) -> ran ( S ++ T ) = ( ran S u. ran T ) )

Proof

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