Metamath Proof Explorer

Theorem ccatsymb

Description: The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018) (Proof shortened by AV, 24-Nov-2018)

Ref Expression
Assertion ccatsymb 
|- ( ( A e. Word V /\ B e. Word V /\ I e. ZZ ) -> ( ( A ++ B ) ` I ) = if ( I < ( # ` A ) , ( A ` I ) , ( B ` ( I - ( # ` A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simprll 
 |-  ( ( 0 <_ I /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) ) -> ( A e. Word V /\ B e. Word V ) )
2 simpr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) -> I < ( # ` A ) )
3 2 anim2i 
 |-  ( ( 0 <_ I /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) ) -> ( 0 <_ I /\ I < ( # ` A ) ) )
4 simpr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> I e. ZZ )
5 0zd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> 0 e. ZZ )
6 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
7 6 nn0zd 
 |-  ( A e. Word V -> ( # ` A ) e. ZZ )
8 7 ad2antrr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( # ` A ) e. ZZ )
9 elfzo 
 |-  ( ( I e. ZZ /\ 0 e. ZZ /\ ( # ` A ) e. ZZ ) -> ( I e. ( 0 ..^ ( # ` A ) ) <-> ( 0 <_ I /\ I < ( # ` A ) ) ) )
10 4 5 8 9 syl3anc 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( I e. ( 0 ..^ ( # ` A ) ) <-> ( 0 <_ I /\ I < ( # ` A ) ) ) )
11 10 ad2antrl 
 |-  ( ( 0 <_ I /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) ) -> ( I e. ( 0 ..^ ( # ` A ) ) <-> ( 0 <_ I /\ I < ( # ` A ) ) ) )
12 3 11 mpbird 
 |-  ( ( 0 <_ I /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) ) -> I e. ( 0 ..^ ( # ` A ) ) )
13 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ( 0 ..^ ( # ` A ) ) ) <-> ( ( A e. Word V /\ B e. Word V ) /\ I e. ( 0 ..^ ( # ` A ) ) ) )
14 1 12 13 sylanbrc 
 |-  ( ( 0 <_ I /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) ) -> ( A e. Word V /\ B e. Word V /\ I e. ( 0 ..^ ( # ` A ) ) ) )
15 ccatval1 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` I ) = ( A ` I ) )
16 15 eqcomd 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` I ) = ( ( A ++ B ) ` I ) )
17 14 16 syl 
 |-  ( ( 0 <_ I /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) ) -> ( A ` I ) = ( ( A ++ B ) ` I ) )
18 17 ex 
 |-  ( 0 <_ I -> ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) -> ( A ` I ) = ( ( A ++ B ) ` I ) ) )
19 zre 
 |-  ( I e. ZZ -> I e. RR )
20 0red 
 |-  ( I e. ZZ -> 0 e. RR )
21 19 20 ltnled 
 |-  ( I e. ZZ -> ( I < 0 <-> -. 0 <_ I ) )
22 21 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( I < 0 <-> -. 0 <_ I ) )
23 simpl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> A e. Word V )
24 23 anim1i 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( A e. Word V /\ I e. ZZ ) )
25 24 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( A e. Word V /\ I e. ZZ ) )
26 animorrl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( I < 0 \/ ( # ` A ) <_ I ) )
27 wrdsymb0 
 |-  ( ( A e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ ( # ` A ) <_ I ) -> ( A ` I ) = (/) ) )
28 25 26 27 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( A ` I ) = (/) )
29 ccatcl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
30 29 anim1i 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( A ++ B ) e. Word V /\ I e. ZZ ) )
31 30 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( ( A ++ B ) e. Word V /\ I e. ZZ ) )
32 animorrl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( I < 0 \/ ( # ` ( A ++ B ) ) <_ I ) )
33 wrdsymb0 
 |-  ( ( ( A ++ B ) e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ ( # ` ( A ++ B ) ) <_ I ) -> ( ( A ++ B ) ` I ) = (/) ) )
34 31 32 33 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( ( A ++ B ) ` I ) = (/) )
35 28 34 eqtr4d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < 0 ) -> ( A ` I ) = ( ( A ++ B ) ` I ) )
36 35 ex 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( I < 0 -> ( A ` I ) = ( ( A ++ B ) ` I ) ) )
37 22 36 sylbird 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( -. 0 <_ I -> ( A ` I ) = ( ( A ++ B ) ` I ) ) )
38 37 com12 
 |-  ( -. 0 <_ I -> ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( A ` I ) = ( ( A ++ B ) ` I ) ) )
39 38 adantrd 
 |-  ( -. 0 <_ I -> ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) -> ( A ` I ) = ( ( A ++ B ) ` I ) ) )
40 18 39 pm2.61i 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ I < ( # ` A ) ) -> ( A ` I ) = ( ( A ++ B ) ` I ) )
41 simprll 
 |-  ( ( I < ( ( # ` A ) + ( # ` B ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) ) -> ( A e. Word V /\ B e. Word V ) )
42 id 
 |-  ( I < ( ( # ` A ) + ( # ` B ) ) -> I < ( ( # ` A ) + ( # ` B ) ) )
43 6 nn0red 
 |-  ( A e. Word V -> ( # ` A ) e. RR )
44 lenlt 
 |-  ( ( ( # ` A ) e. RR /\ I e. RR ) -> ( ( # ` A ) <_ I <-> -. I < ( # ` A ) ) )
45 43 19 44 syl2an 
 |-  ( ( A e. Word V /\ I e. ZZ ) -> ( ( # ` A ) <_ I <-> -. I < ( # ` A ) ) )
46 45 adantlr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( # ` A ) <_ I <-> -. I < ( # ` A ) ) )
47 46 biimpar 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) -> ( # ` A ) <_ I )
48 42 47 anim12ci 
 |-  ( ( I < ( ( # ` A ) + ( # ` B ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) ) -> ( ( # ` A ) <_ I /\ I < ( ( # ` A ) + ( # ` B ) ) ) )
49 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
50 49 nn0zd 
 |-  ( B e. Word V -> ( # ` B ) e. ZZ )
51 zaddcl 
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
52 7 50 51 syl2an 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
53 52 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
54 elfzo 
 |-  ( ( I e. ZZ /\ ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ ) -> ( I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( ( # ` A ) <_ I /\ I < ( ( # ` A ) + ( # ` B ) ) ) ) )
55 4 8 53 54 syl3anc 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( ( # ` A ) <_ I /\ I < ( ( # ` A ) + ( # ` B ) ) ) ) )
56 55 ad2antrl 
 |-  ( ( I < ( ( # ` A ) + ( # ` B ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) ) -> ( I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( ( # ` A ) <_ I /\ I < ( ( # ` A ) + ( # ` B ) ) ) ) )
57 48 56 mpbird 
 |-  ( ( I < ( ( # ` A ) + ( # ` B ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) ) -> I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
58 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) <-> ( ( A e. Word V /\ B e. Word V ) /\ I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
59 41 57 58 sylanbrc 
 |-  ( ( I < ( ( # ` A ) + ( # ` B ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) ) -> ( A e. Word V /\ B e. Word V /\ I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
60 ccatval2 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` I ) = ( B ` ( I - ( # ` A ) ) ) )
61 60 eqcomd 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) )
62 59 61 syl 
 |-  ( ( I < ( ( # ` A ) + ( # ` B ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) )
63 62 ex 
 |-  ( I < ( ( # ` A ) + ( # ` B ) ) -> ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) ) )
64 49 nn0red 
 |-  ( B e. Word V -> ( # ` B ) e. RR )
65 readdcl 
 |-  ( ( ( # ` A ) e. RR /\ ( # ` B ) e. RR ) -> ( ( # ` A ) + ( # ` B ) ) e. RR )
66 43 64 65 syl2an 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` A ) + ( # ` B ) ) e. RR )
67 lenlt 
 |-  ( ( ( ( # ` A ) + ( # ` B ) ) e. RR /\ I e. RR ) -> ( ( ( # ` A ) + ( # ` B ) ) <_ I <-> -. I < ( ( # ` A ) + ( # ` B ) ) ) )
68 66 19 67 syl2an 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( ( # ` A ) + ( # ` B ) ) <_ I <-> -. I < ( ( # ` A ) + ( # ` B ) ) ) )
69 simplr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> B e. Word V )
70 simpr 
 |-  ( ( A e. Word V /\ I e. ZZ ) -> I e. ZZ )
71 7 adantr 
 |-  ( ( A e. Word V /\ I e. ZZ ) -> ( # ` A ) e. ZZ )
72 70 71 zsubcld 
 |-  ( ( A e. Word V /\ I e. ZZ ) -> ( I - ( # ` A ) ) e. ZZ )
73 72 adantlr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( I - ( # ` A ) ) e. ZZ )
74 69 73 jca 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( B e. Word V /\ ( I - ( # ` A ) ) e. ZZ ) )
75 74 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( B e. Word V /\ ( I - ( # ` A ) ) e. ZZ ) )
76 43 ad2antrr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( # ` A ) e. RR )
77 64 ad2antlr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( # ` B ) e. RR )
78 19 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> I e. RR )
79 76 77 78 leaddsub2d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( ( # ` A ) + ( # ` B ) ) <_ I <-> ( # ` B ) <_ ( I - ( # ` A ) ) ) )
80 79 biimpa 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( # ` B ) <_ ( I - ( # ` A ) ) )
81 80 olcd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( ( I - ( # ` A ) ) < 0 \/ ( # ` B ) <_ ( I - ( # ` A ) ) ) )
82 wrdsymb0 
 |-  ( ( B e. Word V /\ ( I - ( # ` A ) ) e. ZZ ) -> ( ( ( I - ( # ` A ) ) < 0 \/ ( # ` B ) <_ ( I - ( # ` A ) ) ) -> ( B ` ( I - ( # ` A ) ) ) = (/) ) )
83 75 81 82 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( B ` ( I - ( # ` A ) ) ) = (/) )
84 30 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( ( A ++ B ) e. Word V /\ I e. ZZ ) )
85 ccatlen 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
86 85 ad2antrr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
87 simpr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( ( # ` A ) + ( # ` B ) ) <_ I )
88 86 87 eqbrtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( # ` ( A ++ B ) ) <_ I )
89 88 olcd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( I < 0 \/ ( # ` ( A ++ B ) ) <_ I ) )
90 84 89 33 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( ( A ++ B ) ` I ) = (/) )
91 83 90 eqtr4d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ ( ( # ` A ) + ( # ` B ) ) <_ I ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) )
92 91 ex 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( ( # ` A ) + ( # ` B ) ) <_ I -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) ) )
93 68 92 sylbird 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( -. I < ( ( # ` A ) + ( # ` B ) ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) ) )
94 93 com12 
 |-  ( -. I < ( ( # ` A ) + ( # ` B ) ) -> ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) ) )
95 94 adantrd 
 |-  ( -. I < ( ( # ` A ) + ( # ` B ) ) -> ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) ) )
96 63 95 pm2.61i 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) /\ -. I < ( # ` A ) ) -> ( B ` ( I - ( # ` A ) ) ) = ( ( A ++ B ) ` I ) )
97 40 96 ifeqda 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> if ( I < ( # ` A ) , ( A ` I ) , ( B ` ( I - ( # ` A ) ) ) ) = ( ( A ++ B ) ` I ) )
98 97 eqcomd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ I e. ZZ ) -> ( ( A ++ B ) ` I ) = if ( I < ( # ` A ) , ( A ` I ) , ( B ` ( I - ( # ` A ) ) ) ) )
99 98 3impa 
 |-  ( ( A e. Word V /\ B e. Word V /\ I e. ZZ ) -> ( ( A ++ B ) ` I ) = if ( I < ( # ` A ) , ( A ` I ) , ( B ` ( I - ( # ` A ) ) ) ) )