Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → 𝑊 ∈ Word 𝑉 ) |
2 |
|
s1cl |
⊢ ( 𝑆 ∈ 𝑉 → 〈“ 𝑆 ”〉 ∈ Word 𝑉 ) |
3 |
2
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → 〈“ 𝑆 ”〉 ∈ Word 𝑉 ) |
4 |
|
s1nz |
⊢ 〈“ 𝑆 ”〉 ≠ ∅ |
5 |
4
|
a1i |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → 〈“ 𝑆 ”〉 ≠ ∅ ) |
6 |
|
lswccatn0lsw |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 〈“ 𝑆 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝑆 ”〉 ≠ ∅ ) → ( lastS ‘ ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) = ( lastS ‘ 〈“ 𝑆 ”〉 ) ) |
7 |
1 3 5 6
|
syl3anc |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( lastS ‘ ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) = ( lastS ‘ 〈“ 𝑆 ”〉 ) ) |
8 |
|
lsws1 |
⊢ ( 𝑆 ∈ 𝑉 → ( lastS ‘ 〈“ 𝑆 ”〉 ) = 𝑆 ) |
9 |
8
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( lastS ‘ 〈“ 𝑆 ”〉 ) = 𝑆 ) |
10 |
7 9
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ) → ( lastS ‘ ( 𝑊 ++ 〈“ 𝑆 ”〉 ) ) = 𝑆 ) |