Metamath Proof Explorer

Theorem swrdccatin1

Description: The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018)

Ref Expression
Assertion swrdccatin1 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = 0 → ( 0 ... ( ♯ ‘ 𝐴 ) ) = ( 0 ... 0 ) )
2 1 eleq2d ⊢ ( ( ♯ ‘ 𝐴 ) = 0 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ 𝑁 ∈ ( 0 ... 0 ) ) )
3 elfz1eq ⊢ ( 𝑁 ∈ ( 0 ... 0 ) → 𝑁 = 0 )
4 elfz1eq ⊢ ( 𝑀 ∈ ( 0 ... 0 ) → 𝑀 = 0 )
5 swrd00 ⊢ ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 0 ⟩ ) = ∅
6 swrd00 ⊢ ( 𝐴 substr ⟨ 0 , 0 ⟩ ) = ∅
7 5 6 eqtr4i ⊢ ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 0 ⟩ ) = ( 𝐴 substr ⟨ 0 , 0 ⟩ )
8 opeq1 ⊢ ( 𝑀 = 0 → ⟨ 𝑀 , 0 ⟩ = ⟨ 0 , 0 ⟩ )
9 8 oveq2d ⊢ ( 𝑀 = 0 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 0 ⟩ ) = ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 0 ⟩ ) )
10 8 oveq2d ⊢ ( 𝑀 = 0 → ( 𝐴 substr ⟨ 𝑀 , 0 ⟩ ) = ( 𝐴 substr ⟨ 0 , 0 ⟩ ) )
11 7 9 10 3eqtr4a ⊢ ( 𝑀 = 0 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 0 ⟩ ) )
12 4 11 syl ⊢ ( 𝑀 ∈ ( 0 ... 0 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 0 ⟩ ) )
13 oveq2 ⊢ ( 𝑁 = 0 → ( 0 ... 𝑁 ) = ( 0 ... 0 ) )
14 13 eleq2d ⊢ ( 𝑁 = 0 → ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ 𝑀 ∈ ( 0 ... 0 ) ) )
15 opeq2 ⊢ ( 𝑁 = 0 → ⟨ 𝑀 , 𝑁 ⟩ = ⟨ 𝑀 , 0 ⟩ )
16 15 oveq2d ⊢ ( 𝑁 = 0 → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 0 ⟩ ) )
17 15 oveq2d ⊢ ( 𝑁 = 0 → ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 0 ⟩ ) )
18 16 17 eqeq12d ⊢ ( 𝑁 = 0 → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ↔ ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 0 ⟩ ) ) )
19 14 18 imbi12d ⊢ ( 𝑁 = 0 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ↔ ( 𝑀 ∈ ( 0 ... 0 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 0 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 0 ⟩ ) ) ) )
20 12 19 mpbiri ⊢ ( 𝑁 = 0 → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
21 3 20 syl ⊢ ( 𝑁 ∈ ( 0 ... 0 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
22 2 21 biimtrdi ⊢ ( ( ♯ ‘ 𝐴 ) = 0 → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) ) )
23 22 impcomd ⊢ ( ( ♯ ‘ 𝐴 ) = 0 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
24 23 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) = 0 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
25 ccatcl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
26 25 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
27 simprl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
28 elfzelfzccat ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
29 28 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) )
30 29 ad2ant2rl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) )
31 swrdvalfn ⊢ ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
32 26 27 30 31 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
33 3anass ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ↔ ( 𝐴 ∈ Word 𝑉 ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
34 33 simplbi2 ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
35 34 ad2antrr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) )
36 35 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
37 swrdvalfn ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
38 36 37 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
39 simp-4l ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝐴 ∈ Word 𝑉 )
40 simp-4r ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝐵 ∈ Word 𝑉 )
41 elfznn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
42 nn0addcl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 )
43 42 expcom ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑘 ∈ ℕ0 → ( 𝑘 + 𝑀 ) ∈ ℕ0 ) )
44 41 43 syl ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑘 ∈ ℕ0 → ( 𝑘 + 𝑀 ) ∈ ℕ0 ) )
45 44 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝑘 ∈ ℕ0 → ( 𝑘 + 𝑀 ) ∈ ℕ0 ) )
46 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → 𝑘 ∈ ℕ0 )
47 45 46 impel ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑘 + 𝑀 ) ∈ ℕ0 )
48 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
49 elnnne0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
50 49 simplbi2 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐴 ) ≠ 0 → ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
51 48 50 syl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( ♯ ‘ 𝐴 ) ≠ 0 → ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
52 51 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝐴 ) ≠ 0 → ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
53 52 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
54 53 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
55 elfzo0 ⊢ ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) )
56 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) )
57 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
58 57 ad2antrl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑘 ∈ ℝ )
59 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
60 59 ad2antll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑀 ∈ ℝ )
61 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
62 61 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → 𝑁 ∈ ℝ )
63 58 60 62 ltaddsubd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( 𝑘 + 𝑀 ) < 𝑁 ↔ 𝑘 < ( 𝑁 − 𝑀 ) ) )
64 nn0readdcl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 𝑀 ) ∈ ℝ )
65 64 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( 𝑘 + 𝑀 ) ∈ ℝ )
66 nn0re ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
67 66 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℝ )
68 ltletr ⊢ ( ( ( 𝑘 + 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ ) → ( ( ( 𝑘 + 𝑀 ) < 𝑁 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
69 65 62 67 68 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( ( 𝑘 + 𝑀 ) < 𝑁 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
70 69 expd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( ( 𝑘 + 𝑀 ) < 𝑁 → ( 𝑁 ≤ ( ♯ ‘ 𝐴 ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
71 63 70 sylbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ) → ( 𝑘 < ( 𝑁 − 𝑀 ) → ( 𝑁 ≤ ( ♯ ‘ 𝐴 ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
72 71 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 < ( 𝑁 − 𝑀 ) → ( 𝑁 ≤ ( ♯ ‘ 𝐴 ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) )
73 72 com24 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑁 ≤ ( ♯ ‘ 𝐴 ) → ( 𝑘 < ( 𝑁 − 𝑀 ) → ( ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) )
74 73 3impia ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑘 < ( 𝑁 − 𝑀 ) → ( ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
75 74 com13 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑘 < ( 𝑁 − 𝑀 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
76 75 impancom ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) → ( 𝑀 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
77 76 3adant2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) → ( 𝑀 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
78 77 com13 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝑀 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
79 56 78 sylbi ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) → ( 𝑀 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
80 41 79 mpan9 ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
81 80 adantl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ ∧ 𝑘 < ( 𝑁 − 𝑀 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
82 55 81 biimtrid ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
83 82 imp ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) )
84 elfzo0 ⊢ ( ( 𝑘 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( ( 𝑘 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝑘 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
85 47 54 83 84 syl3anbrc ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝑘 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
86 ccatval1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝑘 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑘 + 𝑀 ) ) = ( 𝐴 ‘ ( 𝑘 + 𝑀 ) ) )
87 39 40 85 86 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑘 + 𝑀 ) ) = ( 𝐴 ‘ ( 𝑘 + 𝑀 ) ) )
88 25 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
89 simplrl ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
90 30 adantr ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) )
91 simpr ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
92 swrdfv ⊢ ( ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑘 + 𝑀 ) ) )
93 88 89 90 91 92 syl31anc ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝑘 + 𝑀 ) ) )
94 swrdfv ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( 𝐴 ‘ ( 𝑘 + 𝑀 ) ) )
95 36 94 sylan ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( 𝐴 ‘ ( 𝑘 + 𝑀 ) ) )
96 87 93 95 3eqtr4d ⊢ ( ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝑘 ) )
97 32 38 96 eqfnfvd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
98 97 ex ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )
99 24 98 pm2.61dane ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ) )