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 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ ) → ( ( 𝐴 ++ 𝐵 ) ‘ 𝐼 ) = if ( 𝐼 < ( ♯ ‘ 𝐴 ) , ( 𝐴 ‘ 𝐼 ) , ( 𝐵 ‘ ( 𝐼 − ( ♯ ‘ 𝐴 ) ) ) ) )

Proof

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