Step |
Hyp |
Ref |
Expression |
1 |
|
s4cli |
⊢ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ∈ Word V |
2 |
|
lsw |
⊢ ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ∈ Word V → ( lastS ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) = ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) − 1 ) ) ) |
3 |
1 2
|
mp1i |
⊢ ( 𝐷 ∈ 𝑉 → ( lastS ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) = ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) − 1 ) ) ) |
4 |
|
s4len |
⊢ ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) = 4 |
5 |
4
|
oveq1i |
⊢ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) − 1 ) = ( 4 − 1 ) |
6 |
|
4m1e3 |
⊢ ( 4 − 1 ) = 3 |
7 |
5 6
|
eqtri |
⊢ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) − 1 ) = 3 |
8 |
7
|
fveq2i |
⊢ ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) − 1 ) ) = ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ 3 ) |
9 |
8
|
a1i |
⊢ ( 𝐷 ∈ 𝑉 → ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) − 1 ) ) = ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ 3 ) ) |
10 |
|
s4fv3 |
⊢ ( 𝐷 ∈ 𝑉 → ( 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ‘ 3 ) = 𝐷 ) |
11 |
3 9 10
|
3eqtrd |
⊢ ( 𝐷 ∈ 𝑉 → ( lastS ‘ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ) = 𝐷 ) |