# 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 ${⊢}\left({A}\in \mathrm{Word}{V}\wedge {B}\in \mathrm{Word}{V}\wedge {I}\in ℤ\right)\to \left({A}\mathrm{++}{B}\right)\left({I}\right)=if\left({I}<\left|{A}\right|,{A}\left({I}\right),{B}\left({I}-\left|{A}\right|\right)\right)$

### Proof

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