Step |
Hyp |
Ref |
Expression |
1 |
|
ccatw2s1ass |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ) |
2 |
1
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) = ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ) |
3 |
2
|
fveq1d |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) ‘ 𝐼 ) = ( ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ‘ 𝐼 ) ) |
4 |
|
simp1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑉 ) |
5 |
|
s1cli |
⊢ 〈“ 𝑋 ”〉 ∈ Word V |
6 |
|
ccatws1clv |
⊢ ( 〈“ 𝑋 ”〉 ∈ Word V → ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ∈ Word V ) |
7 |
5 6
|
mp1i |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ∈ Word V ) |
8 |
|
simp2 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ℕ0 ) |
9 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
10 |
9
|
3ad2ant1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
11 |
|
nn0ge0 |
⊢ ( 𝐼 ∈ ℕ0 → 0 ≤ 𝐼 ) |
12 |
11
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → 0 ≤ 𝐼 ) |
13 |
|
0red |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → 0 ∈ ℝ ) |
14 |
|
nn0re |
⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ ) |
15 |
14
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → 𝐼 ∈ ℝ ) |
16 |
9
|
nn0red |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℝ ) |
17 |
16
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℝ ) |
18 |
|
lelttr |
⊢ ( ( 0 ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 0 ≤ 𝐼 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) ) ) |
19 |
13 15 17 18
|
syl3anc |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → ( ( 0 ≤ 𝐼 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) ) ) |
20 |
12 19
|
mpand |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 < ( ♯ ‘ 𝑊 ) → 0 < ( ♯ ‘ 𝑊 ) ) ) |
21 |
20
|
3impia |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) ) |
22 |
|
elnnnn0b |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 0 < ( ♯ ‘ 𝑊 ) ) ) |
23 |
10 21 22
|
sylanbrc |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ ) |
24 |
|
simp3 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 < ( ♯ ‘ 𝑊 ) ) |
25 |
|
elfzo0 |
⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐼 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) ) |
26 |
8 23 24 25
|
syl3anbrc |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
27 |
|
ccatval1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ∈ Word V ∧ 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) ) |
28 |
4 7 26 27
|
syl3anc |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 ++ ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) ) |
29 |
3 28
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < ( ♯ ‘ 𝑊 ) ) → ( ( ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ++ 〈“ 𝑌 ”〉 ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) ) |